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