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

now :: thesis: for r, p1 being Real st r in X & p1 in Y holds
r < p1

let r, p1 be Real; :: 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 such that
A9: for r, p1 being Real st r in X & p1 in Y holds
( r <= g2 & g2 <= p1 ) by Th1;
consider g1 being Real such that
A10: for r being Real st r in X holds
not g1 < r by A4;
g1 in REAL by XREAL_0:def 1;
then A11: g1 in Y by A10, A5;
reconsider g2p = g2 - p as Element of REAL by XREAL_0:def 1;

A12: now :: thesis: g2 - p in Y

assume not g2 - p in Y ; :: thesis: contradiction
then not S₁[g2p] by A5;
then consider r1 being Real such that
A13: ( r1 in X & g2p < r1 ) ;
( (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;
then g2 + (- p) < g2 + 0 by XREAL_1:6;
hence contradiction by A2, A9, A12; :: thesis: verum