theorem Th21: :: MSSUBFAM:21

for I being set
for A being ManySortedSet of I holds
( A is finite-yielding iff bool A is finite-yielding )