let r be real number ; :: thesis: ex n being Element of NAT st r < n
for r being real number st r in NAT holds
r + 1 in NAT by AXIOMS:2;
then consider p being real number such that
A1: p in NAT and
A2: r < p by Th9;
consider n1 being Element of NAT such that
A3: n1 = p by A1;
take n1 ; :: thesis: r < n1
thus r < n1 by A2, A3; :: thesis: verum