per cases ( d = - 1 or d is natural ) by Def11;

suppose d = - 1 ; :: thesis: d + 1 is natural

then d + 1 = 0 ;
hence d + 1 is natural ; :: thesis: verum

end;

suppose d is natural ; :: thesis: d + 1 is natural

hence d + 1 is natural ; :: thesis: verum

end;

end;