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