[[0]] I c= bool M by PBOOLE:43;
then [[0]] I is ManySortedSubset of bool M by PBOOLE:def 18;
hence ex b₁ being MSSubsetFamily of M st
( b₁ is V9() & b₁ is V36() ) ; :: thesis: verum