( n in NAT & k in NAT ) by ORDINAL1:def 12;
hence n + k is natural by AXIOMS:2; :: thesis: verum