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

proof

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;

hence sup X <= sup Y by Def3; :: thesis: verum