defpred S1[ non zero Nat] means ( not $1 is trivial implies P1[$1] );
A3:
now for k being non zero Nat st S1[k] holds
S1[k + 1]let k be non
zero Nat;
( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
S1[k + 1]hence
S1[
k + 1]
;
verum end;
A5:
S1[1]
by Def1;
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A5, A3);
hence
for k being non trivial Nat holds P1[k]
; verum