theorem :: MMLQUERY:41

for X being set
for O being Operation of X holds NOT (NOT (NOT O)) = NOT O