let X be ext-real-membered non empty set ; :: thesis: for x being UpperBound of X st x in X holds

x = sup X

let x be UpperBound of X; :: thesis: ( x in X implies x = sup X )

assume x in X ; :: thesis: x = sup X

then for y being UpperBound of X holds x <= y by Def1;

hence x = sup X by Def3; :: thesis: verum

x = sup X

let x be UpperBound of X; :: thesis: ( x in X implies x = sup X )

assume x in X ; :: thesis: x = sup X

then for y being UpperBound of X holds x <= y by Def1;

hence x = sup X by Def3; :: thesis: verum