theorem :: RELSET_3:20

for z being Complex holds addRel (COMPLEX,z) = { [z1,(z1 + z)] where z1 is Complex : verum }