let eps be ExtReal; :: thesis: for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds
ex x being ExtReal 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 ExtReal st
( x in X & (sup X) - eps < x ) )
assume that
A1: 0. < eps and
A2: sup X is Real ; :: thesis: ex x being ExtReal st
( x in X & (sup X) - eps < x )
A3: sup X in REAL by A2, XREAL_0:def 1;
assume for x being ExtReal 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 A4: 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 Element of REAL by A1, A3, XXREAL_0:48;
a <= a - b by A4, SUPINF_2:3;
hence contradiction by A1, XREAL_1:44; :: thesis: verum

end;

suppose eps = +infty ; :: thesis: contradiction

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

end;

end;