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