theorem :: RELSET_3:39

for n, n1 being Nat holds [n1,(n1 + n)] in addRel (NAT,n)