theorem :: RELSET_3:15
for z being Complex
for X, Y being complex-membered set holds (addRel (X,z)) \/ (addRel (Y,z)) c= addRel ((X \/ Y),z)