let y be ext-real number ; :: thesis: ( y = inf X iff ( y in X & ( for x being ext-real number st x in X holds
y <= x ) ) )
thus ( y = min X implies ( y in X & ( for x being ext-real number st x in X holds
y <= x ) ) ) by Def5, Th3; :: thesis: ( y in X & ( for x being ext-real number st x in X holds
y <= x ) implies y = inf X )
assume that
Z1: y in X and
Z2: for x being ext-real number st x in X holds
y <= x ; :: thesis: y = inf X
A: y is LowerBound of X by Z2, Def2;
for x being LowerBound of X holds x <= y by Z1, Def2;
hence y = inf X by A, Def4; :: thesis: verum