let x be set ; :: according to PRALG_1:def 11 :: thesis: ( not x in proj1 (MSSet P,Q) or (MSSet P,Q) . x is 1-sorted )
assume x in dom (MSSet P,Q) ; :: thesis: (MSSet P,Q) . x is 1-sorted
then x in {0 ,1} by FUNCT_4:65;
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence (MSSet P,Q) . x is 1-sorted by FUNCT_4:66; :: thesis: verum