theorem :: MBOOLEAN:10

for I being set
for A, B being ManySortedSet of I holds bool (A (\) B) c= (I --> {{}}) (\/) ((bool A) (\) (bool B))