theorem Th37: :: MMLQUERY:37

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