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