let x be TolStr ; :: according to PCS_0:def 16 :: thesis: ( x in rng (MSSet (P,Q)) implies x is pcs-tol-reflexive )
assume x in rng (MSSet (P,Q)) ; :: thesis: x is pcs-tol-reflexive
then x in {P,Q} by FUNCT_4:64;
hence x is pcs-tol-reflexive by TARSKI:def 2; :: thesis: verum