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