let P, Q be TolStr ; :: thesis: ( TolStr(# the carrier of P,the ToleranceRel of P #) = TolStr(# the carrier of Q,the ToleranceRel of Q #) & P is pcs-tol-symmetric implies Q is pcs-tol-symmetric )
assume that
A1: TolStr(# the carrier of P,the ToleranceRel of P #) = TolStr(# the carrier of Q,the ToleranceRel of Q #) and
A2: the ToleranceRel of P is_symmetric_in the carrier of P ; :: according to PCS_0:def 11 :: thesis: Q is pcs-tol-symmetric
let x, y be set ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( not x in the carrier of Q or not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q )
assume x in the carrier of Q ; :: thesis: ( not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q )
hence ( not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q ) by A1, A2, RELAT_2:def 3; :: thesis: verum