EmptyMS I c= bool M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of bool M by PBOOLE:def 18;
hence ex b₁ being MSSubsetFamily of M st
( b₁ is empty-yielding & b₁ is finite-yielding ) ; :: thesis: verum