defpred S₁[ Nat] means a +^ a is natural ;

A1: now :: thesis: for b being Nat st S₁[b] holds
S₁[ succ b]

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

end;

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