for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y st Y c= REAL holds
( F is bounded_below iff inf F in REAL )