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 ( sup F < +infty & -infty < inf F ) ; :: thesis: F is bounded
then ( F is bounded_above & F is bounded_below ) by Def11, Def12;
hence F is bounded ; :: thesis: verum