theorem :: MMLQUERY:31

for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 AND O2) = (x . O1) AND (x . O2) by RELSET_2:11;