[0] I c= bool M by PBOOLE:49;
then [0] I is ManySortedSubset of bool M by PBOOLE:def 23;
hence ex b₁ being MSSubsetFamily of M st
( b₁ is empty-yielding & b₁ is finite-yielding ) ; :: thesis: verum