bool M is ManySortedSubset of bool M by PBOOLE:def 18;
hence not for b₁ being MSSubsetFamily of M holds b₁ is non-empty ; :: thesis: verum