theorem :: CLOSURE3:12

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