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

( 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