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 = sup Y )
let Y be non empty Subset of REAL ; :: thesis: ( X = Y & Y is bounded_above implies ( X is bounded_above & sup X = sup Y ) )
assume that
A1: X = Y and
A2: Y is bounded_above ; :: thesis: ( X is bounded_above & sup X = sup Y )
for r being ext-real number st r in X holds
r <= sup Y by A1, A2, SEQ_4:def 4;
then A4: upper_bound Y is UpperBound of X by XXREAL_2:def 1;
hence A5: X is bounded_above by SUPINF_1:def 11; :: thesis: sup X = sup Y
A6: sup X <= sup Y by A4, XXREAL_2:def 3;
not -infty in X by A1;
then X <> {-infty } by TARSKI:def 1;
then B7: sup X in REAL by A5, XXREAL_2:57;
for s being real number st s in Y holds
s <= sup X by A1, XXREAL_2:4;
then sup Y <= sup X by B7, SEQ_4:62;
hence sup Y = sup X by A6, XXREAL_0:1; :: thesis: verum