let y be ExtReal; :: thesis: ( y = inf X iff ( y in X & ( for x being ExtReal st x in X holds
y <= x ) ) )
thus ( y = min X implies ( y in X & ( for x being ExtReal st x in X holds
y <= x ) ) ) by Def5, Th3; :: thesis: ( y in X & ( for x being ExtReal st x in X holds
y <= x ) implies y = inf X )
assume that
A1: y in X and
A2: for x being ExtReal st x in X holds
y <= x ; :: thesis: y = inf X
A3: for x being LowerBound of X holds x <= y by A1, Def2;
y is LowerBound of X by A2, Def2;
hence y = inf X by A3, Def4; :: thesis: verum