let y be ExtReal; :: thesis: ( y = sup X iff ( y in X & ( for x being ExtReal st x in X holds
x <= y ) ) )
thus ( y = max X implies ( y in X & ( for x being ExtReal st x in X holds
x <= y ) ) ) by Def6, Th4; :: thesis: ( y in X & ( for x being ExtReal st x in X holds
x <= y ) implies y = sup X )
assume that
A1: y in X and
A2: for x being ExtReal st x in X holds
x <= y ; :: thesis: y = sup X
A3: for x being UpperBound of X holds y <= x by A1, Def1;
y is UpperBound of X by A2, Def1;
hence y = sup X by A3, Def3; :: thesis: verum