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_below iff - F is bounded_above )
let Y be non empty Subset of ExtREAL ; :: thesis: for F being Function of X,Y holds
( F is bounded_below iff - F is bounded_above )
let F be Function of X,Y; :: thesis: ( F is bounded_below iff - F is bounded_above )

hereby :: thesis: ( - F is bounded_above implies F is bounded_below )

assume F is bounded_below ; :: thesis: - F is bounded_above
then -infty < inf F by Def12;
then - (inf F) < - -infty by XXREAL_3:40;
then sup (- F) < +infty by Th38, XXREAL_3:5;
hence - F is bounded_above by Def11; :: thesis: verum

end;

assume - F is bounded_above ; :: thesis: F is bounded_below
then sup (- F) < +infty by Def11;
then - (inf F) < +infty by Th38;
then A1: - +infty < - (- (inf F)) by XXREAL_3:40;
( - +infty = -infty & - (- (inf F)) = inf F ) by XXREAL_3:def 3;
hence F is bounded_below by A1, Def12; :: thesis: verum