let r be Real; :: thesis: ex n being Nat st r < n
for r being Real st r in NAT holds
r + 1 in NAT by AXIOMS:2;
then consider p being Real such that
A1: p in NAT and
A2: r < p by Th2, NUMBERS:19;
consider n1 being Nat such that
A3: n1 = p by A1;
take n1 ; :: thesis: r < n1
thus r < n1 by A2, A3; :: thesis: verum