theorem :: MMLQUERY:34

for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 | O2) = (x . O1) | O2 by RELAT_1:126;