theorem Th17: :: RELSET_3:17

for z1, z2 being Complex
for X being complex-membered set holds (addRel (X,z1)) * (addRel (X,z2)) c= addRel (X,(z1 + z2))