:: deftheorem defines bounded_above MEASURE6:def 11 :
for X being set
for f being Function of X,REAL holds
( f is bounded_above iff f .: X is bounded_above );