More bounding box blatherskeit

The previous definition of bounding box, or something mildly similar, could also arise from adding two additional elements to the domain of `⊴` — call them `⊴_bot` and `⊴_top` — which act respectively as a global infimum and supremum on `⊴`. These elements have a natural representation in `bbb F^n` (where `bbb F` is the set of IEEE floating-point numbers, of whatever precision is relevant) as, respectively, {-Inf, -Inf, ... -Inf} and {+Inf, +Inf, ... +Inf}.

This would imply the existence of semi-infinite bounding boxes extending either positivewards or negativewards on all axes, as well as the existence of the "world box" as the `sube`-supremum. However, the null box would still not be a bounding box under this definition; and the semi-infinite boxes don't have much use for, er, actually computing the bounding boxes of objects or sets. (The world box is at least a useful initial value for foldr `^^`!)

However, in vector spaces constructed as products of sets with with minimal and maximal elements — such as `[0, 2^{:2^{:n:}:}-1] nn NN` or the aforementioned `bbb F` — the local equivalent of `⊴` is already a bounded lattice, naturally yielding the `sube`-supremum as a bounding box in that space without defining it specially.

My initial definition — refined from the above `{⊴_bot, ⊴_top}`-conjoinment, which was itself refined into the definition in the previous entry — was closer to the actual final representation. Perhaps it would be more natural to study the behaviour of posets of pairs of points from lattices, like the representation itself, than to consider "boxes" to be actual delimited sets of points?