theorem :: MEASURE6:42

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