let k be Nat; :: thesis: P₁[k]
consider X being Subset of NAT such that
A3: for x being Element of NAT holds
( x in X iff P₁[x] ) from SUBSET_1:sch 3();
A4: for x being Real st x in X holds
x + 1 in X

proof

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
A5: P₁[k] and
A6: k = x by A3;
P₁[k + 1] by A2, A5;
hence x + 1 in X by A3, A6; :: thesis: verum

end;

( X c= NAT & NAT c= REAL ) by NUMBERS:19;
then X is Subset of REAL by XBOOLE_1:1;
then k in X by A1, A3, A4, Th1;
hence P₁[k] by A3; :: thesis: verum