theorem :: MMLQUERY:42

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