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

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

assume F is bounded_above ; :: thesis: - F is bounded_below
then A1: - +infty < - (sup F) by XXREAL_3:38;
- +infty = -infty by XXREAL_3:def 3;
hence - F is bounded_below by A1, Th19; :: thesis: verum

end;

assume - F is bounded_below ; :: thesis: F is bounded_above
then - (inf (- F)) < - -infty by XXREAL_3:38;
then - (- (sup F)) < - -infty by Th19;
hence F is bounded_above by XXREAL_3:5; :: thesis: verum