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

( 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