:: deftheorem defines (\+\) PBOOLE:def 9 :
for I being set
for X, Y being ManySortedSet of I holds X (\+\) Y = (X (\) Y) (\/) (Y (\) X);