let p be real number ; :: thesis: for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )
let X be Subset of REAL ; :: thesis: ( 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) implies for g being real number ex r being real number st
( r in X & g < r ) )
assume that
A1: 0 < p and
A2: ex r being real number st r in X and
A3: for r being real number st r in X holds
r + p in X and
A4: ex g being real number st
for r being real number st r in X holds
not g < r ; :: thesis: contradiction
consider g1 being real number such that
A5: for r being real number st r in X holds
not g1 < r by A4;
defpred S₁[ Real] means for r being real number st r in X holds
not $1 < r;
consider Y being Subset of REAL such that
A6: for p1 being Real holds
( p1 in Y iff S₁[p1] ) from SUBSET_1:sch 3();
g1 is Real by XREAL_0:def 1;
then A7: g1 in Y by A5, A6;

now

let r, p1 be real number ; :: thesis: ( r in X & p1 in Y implies r < p1 )
assume that
A8: r in X and
A9: p1 in Y ; :: thesis: r < p1
A10: r + p in X by A3, A8;
A11: r + 0 < r + p by A1, XREAL_1:10;
r + p <= p1 by A6, A9, A10;
hence r < p1 by A11, XXREAL_0:2; :: thesis: verum

end;

then consider g2 being real number such that
A12: for r, p1 being real number st r in X & p1 in Y holds
( r <= g2 & g2 <= p1 ) by Th8;
A13: g2 - p is Real by XREAL_0:def 1;

A14: now

assume not g2 - p in Y ; :: thesis: contradiction
then consider r1 being real number such that
A15: r1 in X and
A16: g2 - p < r1 by A6, A13;
A17: (g2 - p) + p < r1 + p by A16, XREAL_1:8;
r1 + p in X by A3, A15;
hence contradiction by A7, A12, A17; :: thesis: verum

end;

- p < - 0 by A1, XREAL_1:26;
then g2 + (- p) < g2 + 0 by XREAL_1:8;
hence contradiction by A2, A12, A14; :: thesis: verum