bool M is ManySortedSubset of bool M by PBOOLE:def 23;
hence ex b₁ being MSSubsetFamily of M st b₁ is non-empty ; :: thesis: verum