let eps be ExtReal; :: thesis: for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds
ex x being ExtReal st
( x in X & x < (inf X) + eps )
let X be non empty Subset of ExtREAL; :: thesis: ( 0. < eps & inf X is Real implies ex x being ExtReal st
( x in X & x < (inf X) + eps ) )
assume that
A1: 0. < eps and
A2: inf X is Real ; :: thesis: ex x being ExtReal st
( x in X & x < (inf X) + eps )
A3: inf X in REAL by A2, XREAL_0:def 1;
assume for x being ExtReal holds
( not x in X or not x < (inf X) + eps ) ; :: thesis: contradiction
then (inf X) + eps is LowerBound of X by XXREAL_2:def 2;
then A4: (inf X) + eps <= inf X by XXREAL_2:def 4;

per cases ( eps < +infty or eps = +infty ) by XXREAL_0:4;

suppose eps < +infty ; :: thesis: contradiction

then reconsider a = inf X, b = eps as Element of REAL by A1, A3, XXREAL_0:48;
(inf X) + eps = a + b by SUPINF_2:1;
then b <= a - a by A4, XREAL_1:19;
hence contradiction by A1; :: thesis: verum

end;

suppose eps = +infty ; :: thesis: contradiction

then (inf X) + eps = +infty by A3, XXREAL_3:def 2;
hence contradiction by A3, A4, XXREAL_0:4; :: thesis: verum

end;

end;