theorem :: MSSUBFAM:31

for I being set
for M being ManySortedSet of I holds EmptyMS I is V9() V39() MSSubsetFamily of M by PBOOLE:43, PBOOLE:def 18;