theorem :: MBOOLEAN:13

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