:: deftheorem Def5 defines bounded_above SUPINF_2:def 5 :
for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded_above iff sup F < +infty );