let x be set ; :: according to PCS_0:def 33 :: thesis: ( x in {0 ,1} implies (MSSet P,Q) . x is pcs )
assume x in {0 ,1} ; :: thesis: (MSSet P,Q) . x is pcs
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence (MSSet P,Q) . x is pcs by FUNCT_4:66; :: thesis: verum