theorem :: MSSUBFAM:19

for I being set
for A, B being ManySortedSet of I st B is non-empty & [|A,B|] is finite-yielding holds
A is finite-yielding