for X being Subset of REAL holds
( X is bounded_above iff -- X is bounded_below )