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;