let M be ExtNat; :: thesis: ( M = sup X iff ( M in X & ( for N being ExtNat st N in X holds
N <= M ) ) )
thus ( M = max X implies ( M in X & ( for N being ExtNat st N in X holds
N <= M ) ) ) by XXREAL_2:def 8; :: thesis: ( M in X & ( for N being ExtNat st N in X holds
N <= M ) implies M = sup X )
assume A1: ( M in X & ( for N being ExtNat st N in X holds
N <= M ) ) ; :: thesis: M = sup X
then for x being ExtReal st x in X holds
x <= M ;
hence M = sup X by A1, XXREAL_2:def 8; :: thesis: verum