:: deftheorem defines bounded SUPINF_2:def 7 :
for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded iff ( F is bounded_above & F is bounded_below ) );