defpred S₁[ Real] means for r being real number st r in NAT holds
not $1 < r;
let r be real number ; :: thesis: ex n being Element of NAT st r < n
consider Y being Subset of REAL such that
A1: for p1 being Real holds
( p1 in Y iff S₁[p1] ) from SUBSET_1:sch 3();
for r, p1 being real number st r in NAT & p1 in Y holds
r <= p1 by A1;
then consider g2 being real number such that
A2: for r, p being real number st r in NAT & p in Y holds
( r <= g2 & g2 <= p ) by AXIOMS:1;
A3: g2 + (- 1) < g2 + 0 by XREAL_1:6;
for g being real number ex r being real number st
( r in NAT & g < r )

proof

given g1 being real number such that A4: for r being real number st r in NAT holds
not g1 < r ; :: thesis: contradiction
g1 is Real by XREAL_0:def 1;
then A5: g1 in Y by A1, A4;

now

assume not g2 - 1 in Y ; :: thesis: contradiction
then consider r1 being real number such that
A6: r1 in NAT and
A7: g2 - 1 < r1 by A1;
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 number 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