theorem :: RELSET_3:14

for z being Complex
for X, Y being complex-membered set holds addRel ((X /\ Y),z) = (addRel (X,z)) /\ (addRel (Y,z))