let X be non empty Subset of ExtREAL; :: thesis: for Y being non empty Subset of REAL st X = Y & Y is bounded_above holds
( X is bounded_above & sup X = upper_bound Y )
let Y be non empty Subset of REAL; :: thesis: ( X = Y & Y is bounded_above implies ( X is bounded_above & sup X = upper_bound Y ) )
assume that
A1: X = Y and
A2: Y is bounded_above ; :: thesis: ( X is bounded_above & sup X = upper_bound Y )
A3: for s being Real st s in Y holds
s <= sup X by A1, XXREAL_2:4;
not -infty in X by A1;
then A4: X <> {-infty} by TARSKI:def 1;
for r being ExtReal st r in X holds
r <= upper_bound Y by A1, A2, SEQ_4:def 1;
then A5: upper_bound Y is UpperBound of X by XXREAL_2:def 1;
hence X is bounded_above by XXREAL_2:def 10; :: thesis: sup X = upper_bound Y
then sup X in REAL by A4, XXREAL_2:57;
then A6: upper_bound Y <= sup X by A3, SEQ_4:45;
sup X <= upper_bound Y by A5, XXREAL_2:def 3;
hence sup X = upper_bound Y by A6, XXREAL_0:1; :: thesis: verum