let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y st Y c= REAL holds
( F is bounded iff ( inf F in REAL & sup F in REAL ) )
let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y st Y c= REAL holds
( F is bounded iff ( inf F in REAL & sup F in REAL ) )
let F be Function of X,Y; :: thesis: ( Y c= REAL implies ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) )
assume A1: Y c= REAL ; :: thesis: ( F is bounded iff ( inf F in REAL & sup F in REAL ) )
hence ( F is bounded implies ( inf F in REAL & sup F in REAL ) ) by Th46, Th47; :: thesis: ( inf F in REAL & sup F in REAL implies F is bounded )
assume that
A2: inf F in REAL and
A3: sup F in REAL ; :: thesis: F is bounded
A4: F is bounded_below by A1, A2, Th47;
F is bounded_above by A1, A3, Th46;
hence F is bounded by A4; :: thesis: verum