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

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