let X be ext-real-membered set ; :: thesis: for x being ExtReal st ex y being ExtReal st
( y in X & x <= y ) holds
x <= sup X
let x be ExtReal; :: thesis: ( ex y being ExtReal st
( y in X & x <= y ) implies x <= sup X )
given y being ExtReal such that A1: y in X and
A2: x <= y ; :: thesis: x <= sup X
y <= sup X by A1, Th4;
hence x <= sup X by A2, XXREAL_0:2; :: thesis: verum