let X be ext-real-membered set ; :: thesis: for x being ext-real number st ex y being ext-real number st
( y in X & x <= y ) holds
x <= sup X
let x be ext-real number ; :: thesis: ( ex y being ext-real number st
( y in X & x <= y ) implies x <= sup X )
given y being ext-real number 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