theorem :: MMLQUERY:32
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 OR O2) = (x . O1) OR (x . O2) by RELSET_2:10;