theorem :: MEASURE6:50

for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )