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

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