theorem Th30: :: RELAT_1:36
for P, Q, R being Relation holds (P * R) * Q = P * (R * Q)