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-reflexive implies Q is pcs-tol-reflexive )
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_reflexive_in the carrier of P ; :: according to PCS_0:def 9 :: thesis: Q is pcs-tol-reflexive
let x be set ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of Q or [^,^] in the ToleranceRel of Q )
assume x in the carrier of Q ; :: thesis: [^,^] in the ToleranceRel of Q
hence [^,^] in the ToleranceRel of Q by A1, A2, RELAT_2:def 1; :: thesis: verum