theorem :: MBOOLEAN:35

for I being set
for A, X being ManySortedSet of I
for B being non-empty ManySortedSet of I st X c= union (A (\/) B) & ( for Y being ManySortedSet of I st Y in B holds
Y (/\) X = EmptyMS I ) holds
X c= union A