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 )

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

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_below
; :: thesis: 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;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

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