theorem :: MBOOLEAN:11

for I being set
for A, B, X being ManySortedSet of I holds
( X c= A (\) B iff ( X c= A & X misses B ) )