theorem :: RELSET_3:40

for n being Nat holds addRel (NAT,n) = { [n1,(n1 + n)] where n1 is Nat : verum }