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