:: deftheorem Def15 defines NOT MMLQUERY:def 15 :
for X being set
for O, b₃ being Operation of X holds
( b₃ = NOT O iff for L being List of X holds L | b₃ = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } );