let P be non empty pcs-Str ; :: thesis: 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; :: thesis: 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); :: thesis: ( p = p9 & q = q9 & not p9 (--) q9 implies p (--) q )
assume that
A1: p = p9 and
A2: q = q9 ; :: thesis: ( 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) ; :: according to PCS_0:def 7 :: thesis: 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; :: according to PCS_0:def 7 :: thesis: verum