let X be non empty set ; :: thesis: 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 ) )
let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y holds
( F is bounded iff ( sup F < +infty & -infty < inf F ) )
let F be Function of X,Y; :: thesis: ( F is bounded iff ( sup F < +infty & -infty < inf F ) )
thus ( F is bounded implies ( sup F < +infty & -infty < inf F ) ) by Def11, Def12; :: thesis: ( sup F < +infty & -infty < inf F implies F is bounded )
assume that
A1: sup F < +infty and
A2: -infty < inf F ; :: thesis: F is bounded
A3: F is bounded_below by A2, Def12;
F is bounded_above by A1, Def11;
hence F is bounded by A3; :: thesis: verum