theorem :: MBOOLEAN:34

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