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