theorem Th41: :: MEASURE6:41

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