let X, Y be ext-real-membered set ; :: thesis: ( ( for x being ExtReal st x in X holds

ex y being ExtReal st

( y in Y & x <= y ) ) implies sup X <= sup Y )

assume A1: for x being ExtReal st x in X holds

ex y being ExtReal st

( y in Y & x <= y ) ; :: thesis: sup X <= sup Y

sup Y is UpperBound of X

ex y being ExtReal st

( y in Y & x <= y ) ) implies sup X <= sup Y )

assume A1: for x being ExtReal st x in X holds

ex y being ExtReal st

( y in Y & x <= y ) ; :: thesis: sup X <= sup Y

sup Y is UpperBound of X

proof

hence
sup X <= sup Y
by Def3; :: thesis: verum
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= sup Y )

assume x in X ; :: thesis: x <= sup Y

then consider y being ExtReal such that

A2: y in Y and

A3: x <= y by A1;

y <= sup Y by A2, Th4;

hence x <= sup Y by A3, XXREAL_0:2; :: thesis: verum

end;assume x in X ; :: thesis: x <= sup Y

then consider y being ExtReal such that

A2: y in Y and

A3: x <= y by A1;

y <= sup Y by A2, Th4;

hence x <= sup Y by A3, XXREAL_0:2; :: thesis: verum