theorem :: MBOOLEAN:12

for I being set
for A, B being ManySortedSet of I holds (bool (A (\) B)) (\/) (bool (B (\) A)) c= bool (A (\+\) B)