theorem Th36: :: MMLQUERY:36

for X being set
for O being Operation of X
for z, s being object holds
( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )