let i be Nat; :: thesis: ( i = 0 or ex k being Nat st i = k + 1 )
defpred S₁[ Nat] means ( $1 = 0 or ex k being Nat st $1 = k + 1 );
A1: for h being Nat st S₁[h] holds
S₁[h + 1] ;
A2: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A1);
hence ( i = 0 or ex k being Nat st i = k + 1 ) ; :: thesis: verum