let k be Nat; :: thesis: ( k is Element of REAL & k is Element of NAT implies P₁[k] )
defpred S₁[ Real] means ex k being Nat st
( P₁[k] & k = $1 );
consider X being Subset of REAL such that
A3: for x being Real holds
( x in X iff S₁[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;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
P₁[k + 1] by A2, A5;
hence x + 1 in X by A3, A6; :: thesis: verum

end;

0 in X by A1, A3;
then k in X by A4, Th1;
then ex n being Nat st
( P₁[n] & n = k ) by A3;
hence ( k is Element of REAL & k is Element of NAT implies P₁[k] ) ; :: thesis: verum