let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y st Y c= REAL holds
( F is bounded_above iff sup F in REAL )
let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y st Y c= REAL holds
( F is bounded_above iff sup F in REAL )
let F be Function of X,Y; :: thesis: ( Y c= REAL implies ( F is bounded_above iff sup F in REAL ) )
assume A1: Y c= REAL ; :: thesis: ( F is bounded_above iff sup F in REAL )

hereby :: thesis: ( sup F in REAL implies F is bounded_above )

set x = the Element of X;
X = dom F by FUNCT_2:def 1;
then A2: F . the Element of X in rng F by FUNCT_1:def 3;
rng F c= Y by RELAT_1:def 19;
then F . the Element of X in Y by A2;
then A3: not sup F = -infty by A1, Th26, XXREAL_0:12;
assume a4: F is bounded_above ; :: thesis: sup F in REAL
( sup F in REAL or sup F in {-infty,+infty} ) by XBOOLE_0:def 3;
hence sup F in REAL by a4, A3, TARSKI:def 2; :: thesis: verum

end;

assume sup F in REAL ; :: thesis: F is bounded_above
hence F is bounded_above by XXREAL_0:9; :: thesis: verum