theorem :: MMLQUERY:43

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