bool M is MSSubsetFamily of M ;
hence ex b₁ being MSSubsetFamily of M st
( b₁ is non-empty & b₁ is finite-yielding ) ; :: thesis: verum