bool M is ManySortedSubset of bool M by PBOOLE:def 18;
hence not for b₁ being MSSubsetFamily of M holds b₁ is V8() ; :: thesis: verum