let i be natural Number ; :: thesis: ( i = 0 or ex k being Nat st i = k + 1 )
A0: i is Nat by TARSKI:1;
defpred S₁[ natural Number ] 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 ) by A0; :: thesis: verum