defpred S₁[ Nat] means ( P₁[$1 + 1] & P₁[$1 + 2] );
A4: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
k + 1 <> 0 + 1 ;
then A5: k + 1 is non trivial Nat by NAT_2:def 1;
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
then P₁[(k + 1) + 1] ;
hence S₁[k + 1] by A3, A5, A6; :: thesis: verum

end;

let k be non trivial Nat; :: thesis: P₁[k]
k <> 1 by NAT_2:def 1;
then A7: k > 1 by NAT_2:19;
then k - 1 > 1 - 1 by XREAL_1:9;
then A8: k - 1 > 0 ;
A9: S₁[1] by A1, A2;
A10: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A9, A4);
(k -' 1) + 1 = k by A7, XREAL_1:235;
hence P₁[k] by A10, A8; :: thesis: verum