:: deftheorem Def6 defines bounded_below SUPINF_2:def 6 :
for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded_below iff -infty < inf F );