theorem Th56: :: FOMODEL0:56

for X being set
for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X)