theorem :: MSSUBFAM:23

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