defpred S₁[ Real] means ex k being Nat st
( n = k & n + k is natural );
consider X being Subset of REAL such that
A1: for x being Real holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();

A2: now

let x be Real; :: thesis: ( x in X implies x + 1 in X )
assume x in X ; :: thesis: x + 1 in X
then consider k being Nat such that
A3: x = k and
A4: n + k is natural by A1;
A5: (n + k) + 1 = n + (k + 1) ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n + k is Element of NAT by A4, ORDINAL1:def 13;
then ( k + 1 is Element of NAT & (n + k) + 1 is Element of NAT ) by AXIOMS:28;
hence x + 1 in X by A1, A3, A5; :: thesis: verum

end;

n + 0 = n ;
then 0 in X by A1;
then k in X by A2, Th1;
then ex m being Nat st
( k = m & n + m is natural ) by A1;
hence n + k is natural ; :: thesis: verum