let y be ext-real number ; :: thesis: ( y = sup X iff ( y in X & ( for x being ext-real number st x in X holds
x <= y ) ) )
thus ( y = max X implies ( y in X & ( for x being ext-real number st x in X holds
x <= y ) ) ) by Def6, Th3B; :: thesis: ( y in X & ( for x being ext-real number st x in X holds
x <= y ) implies y = sup X )
assume that
Z1: y in X and
Z2: for x being ext-real number st x in X holds
x <= y ; :: thesis: y = sup X
A: y is UpperBound of X by Z2, Def1;
for x being UpperBound of X holds y <= x by Z1, Def1;
hence y = sup X by A, Def3; :: thesis: verum