let x be ExtReal; :: thesis: for A being ext-real-membered set st x in A holds
x <= sup A
let A be ext-real-membered set ; :: thesis: ( x in A implies x <= sup A )
sup A is UpperBound of A by Def3;
hence ( x in A implies x <= sup A ) by Def1; :: thesis: verum