theorem :: RELSET_3:19

for z, z1 being Complex holds [z1,(z1 + z)] in addRel (COMPLEX,z)