theorem :: MSSUBFAM:23

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