let n be Nat; :: thesis: ( n = {} or ex m being Nat st n = succ m )
defpred S₁[ Nat] means ( $1 = {} or ex m being Nat st $1 = succ m );
A1: for a being Nat st S₁[a] holds
S₁[ succ a] ;
A2: S₁[ 0 ] ;
thus S₁[n] from ORDINAL2:sch 17(A2, A1); :: thesis: verum