let x be set ; :: according to PCS_0:def 15 :: thesis: ( x in {0,1} implies <%P,Q%> . x is TolStr )
assume x in {0,1} ; :: thesis: <%P,Q%> . x is TolStr
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence <%P,Q%> . x is TolStr ; :: thesis: verum