theorem :: MMLQUERY:53

for X being set
for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2