defpred S₁[ natural number ] means a +^ a is natural ;
A1: S₁[ {} ] by Th44;

A2: now

let b be natural number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume S₁[b] ; :: thesis: S₁[ succ b]
then reconsider c = a +^ b as natural number ;
a +^ (succ b) = succ c by Th45;
hence S₁[ succ b] ; :: thesis: verum

end;

thus S₁[b] from ORDINAL2:sch 17(A1, A2); :: thesis: verum