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 )

hence F is bounded_above by XXREAL_0:9; :: thesis: verum

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 )

assume
sup F in REAL
; :: thesis: 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;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

hence F is bounded_above by XXREAL_0:9; :: thesis: verum