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

hereby :: thesis: ( - F is bounded implies F is bounded )

assume A1: F is bounded ; :: thesis: - F is bounded
then A2: - F is bounded_below by Th40;
- F is bounded_above by A1, Th41;
hence - F is bounded by A2; :: thesis: verum

end;

assume A3: - F is bounded ; :: thesis: F is bounded
then A4: F is bounded_below by Th41;
F is bounded_above by A3, Th40;
hence F is bounded by A4; :: thesis: verum