theorem :: MSSUBFAM:22

for I being set
for A being V8() ManySortedSet of I st A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) holds
union A is V39()