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 - (inf F) < - -infty by XXREAL_3:38;
hence - F is bounded_above by Th19, XXREAL_3:5; :: thesis: verum

end;

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