defpred S₁[ non zero Nat] means ( not $1 is trivial implies P₁[$1] );

A3: now :: thesis:

let k be non zero Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:

now :: thesis:

assume not k + 1 is trivial ; :: thesis:

per cases ;

suppose k = 1 ; :: thesis:

hence S₁[k + 1] by A1; :: thesis:

end;

suppose k <> 1 ; :: thesis:

then not k is trivial ;
hence S₁[k + 1] by A2, A4; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

A5: S₁[1] by Def1;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A5, A3);
hence for k being non trivial Nat holds P₁[k] ; :: thesis: