theorem :: MMLQUERY:33

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