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 )

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

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_above
; :: thesis: 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;then - (inf F) < - -infty by XXREAL_3:38;

hence - F is bounded_above by Th19, XXREAL_3:5; :: thesis: verum

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