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