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
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
A5: for p1 being Real holds
( p1 in Y iff S₁[p1] ) from SUBSET_1:sch 3();

now

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

end;

then consider g2 being real number such that
A9: for r, p1 being real number st r in X & p1 in Y holds
( r <= g2 & g2 <= p1 ) by Th8;
consider g1 being real number such that
A10: for r being real number st r in X holds
not g1 < r by A4;
g1 is Real by XREAL_0:def 1;
then A11: g1 in Y by A10, A5;

A12: now

assume not g2 - p in Y ; :: thesis: contradiction
then consider r1 being real number such that
A13: ( r1 in X & g2 - p < r1 ) by A5;
( (g2 - p) + p < r1 + p & r1 + p in X ) by A3, A13, XREAL_1:6;
hence contradiction by A11, A9; :: thesis: verum

end;

- p < - 0 by A1, XREAL_1:24;
then g2 + (- p) < g2 + 0 by XREAL_1:6;
hence contradiction by A2, A9, A12; :: thesis: verum