defpred S1[ Real] means for r being Real st r in NAT holds
not $1 < r;
let r be Real; :: thesis: ex n being Nat st r < n
consider Y being Subset of REAL such that
A1: for p1 being Element of REAL holds
( p1 in Y iff S1[p1] ) from SUBSET_1:sch 3();
 reconsider N = NAT as Subset of REAL by NUMBERS:19;
for r, p1 being Real st r in N & p1 in Y holds
r <= p1 by A1;
then consider g2 being Real such that
A2: for r, p being Real st r in N & p in Y holds
( r <= g2 & g2 <= p ) by AXIOMS:1;
A3: g2 + (- 1) < g2 + 0 by XREAL_1:6;
for g being Real ex r being Real st
( r in NAT & g < r )
proof
given g1 being Real such that A4: for r being Real st r in NAT holds
not g1 < r ; :: thesis: contradiction
g1 in REAL by XREAL_0:def 1;
then A5: g1 in Y by A1, A4;
now :: thesis: g2 - 1 in Y
reconsider g21 = g2 - 1 as Element of REAL by XREAL_0:def 1;
assume not g2 - 1 in Y ; :: thesis: contradiction
then not S1[g21] by A1;
then consider r1 being Real such that
A6: r1 in NAT and
A7: g2 - 1 < r1 ;
A8: r1 + 1 in NAT by A6, AXIOMS:2;
(g2 - 1) + 1 < r1 + 1 by A7, XREAL_1:6;
hence contradiction by A2, A5, A8; :: thesis: verum
end;
hence contradiction by A2, A3; :: thesis: verum
end;
then consider p being Real such that
A9: p in NAT and
A10: r < p ;
reconsider p = p as Element of NAT by A9;
take p ; :: thesis: r < p
thus r < p by A10; :: thesis: verum