let eps be R_eal; :: thesis: for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds
ex x being ext-real number st
( x in X & (sup X) - eps < x )
let X be non empty Subset of ExtREAL; :: thesis: ( 0. < eps & sup X is Real implies ex x being ext-real number st
( x in X & (sup X) - eps < x ) )
assume that
A1: 0. < eps and
A2: sup X is Real ; :: thesis: ex x being ext-real number st
( x in X & (sup X) - eps < x )
assume for x being ext-real number holds
( not x in X or not (sup X) - eps < x ) ; :: thesis: contradiction
then (sup X) - eps is UpperBound of X by XXREAL_2:def 1;
then A3: sup X <= (sup X) - eps by XXREAL_2:def 3;

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

suppose eps < +infty ; :: thesis: contradiction

then reconsider a = sup X, b = eps as Real by A1, A2, XXREAL_0:48;
a <= a - b by A3, SUPINF_2:3;
hence contradiction by A1, XREAL_1:44; :: thesis: verum

end;

suppose eps = +infty ; :: thesis: contradiction

then (sup X) - eps = -infty by A2, XXREAL_3:13;
hence contradiction by A2, A3, XXREAL_0:6; :: thesis: verum

end;

end;