theorem Th52: :: MMLQUERY:52

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