defpred S₂[ Nat] means $1 = PN-to-NAT . (NAT-to-PN . $1);
A1: S₂[ 0 ] by Lm17;
A2: for n being Nat st S₂[n] holds
S₂[n + 1] by Lm18;
thus for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2); :: thesis: verum