let P be pcs-Str ; :: thesis: for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds
not p9 (--) q9
let p, q be Element of P; :: thesis: for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds
not p9 (--) q9
set R = pcs-reverse P;
let p9, q9 be Element of (pcs-reverse P); :: thesis: ( p = p9 & q = q9 & p (--) q implies not p9 (--) q9 )
assume that
A1: p = p9 and
A2: q = q9 ; :: thesis: ( not p (--) q or not p9 (--) q9 )
A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40;
assume [p,q] in the ToleranceRel of P ; :: according to PCS_0:def 7 :: thesis: not p9 (--) q9
hence not [p9,q9] in the ToleranceRel of (pcs-reverse P) by A1, A2, A3, XBOOLE_0:def 5; :: according to PCS_0:def 7 :: thesis: verum