theorem Th6: :: SYSREL:6

for R, S, T being Relation holds (R \/ S) * T = (R * T) \/ (S * T)