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 F is bounded ; :: thesis: - F is bounded
then ( - F is bounded_above & - F is bounded_below ) by Th40, Th41;
hence - F is bounded ; :: thesis: verum

end;

assume - F is bounded ; :: thesis: F is bounded
then ( F is bounded_above & F is bounded_below ) by Th40, Th41;
hence F is bounded ; :: thesis: verum