theorem :: SUPINF_2:21

for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded iff ( sup F < +infty & -infty < inf F ) ) by Def5, Def6;