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

A3: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now

assume not k + 1 is empty ; :: thesis: S₁[k + 1]
( k is empty or not k is empty ) ;
hence S₁[k + 1] by A1, A2, A4; :: thesis: verum

end;

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

end;

A5: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A3);
hence for k being non empty Nat holds P₁[k] ; :: thesis: verum