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