theorem :: CLOSURE3:13

for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A