theorem :: CLOSURE3:9

for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|