let eps be R_eal; :: thesis: for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds
ex x being ext-real number 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 ext-real number st
( x in X & x < (inf X) + eps ) )
assume A1: ( 0. < eps & inf X is Real ) ; :: thesis: ex x being ext-real number st
( x in X & x < (inf X) + eps )
assume for x being ext-real number 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 A2: (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 Real by A1, XXREAL_0:48;
(inf X) + eps = a + b by SUPINF_2:1;
then b <= a - a by A2, XREAL_1:21;
hence contradiction by A1; :: thesis: verum

end;

suppose eps = +infty ; :: thesis: contradiction

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

end;

end;