theorem :: MSSUBFAM:31

for I being set
for M being ManySortedSet of I holds EmptyMS I is empty-yielding finite-yielding MSSubsetFamily of M by PBOOLE:43, PBOOLE:def 18;