theorem :: CLOSURE3:10

for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)