:: deftheorem defines BUTNOT MMLQUERY:def 18 :
for X being set
for O1, O2, b₄ being Operation of X holds
( b₄ = O1 BUTNOT O2 iff for L being List of X holds L | b₄ = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } );