theorem :: MEASURE6:49

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