let P be non empty pcs-Str ; :: thesis:
let p, q be Element of P; :: thesis:
set R = pcs-reverse P;
let p', q' be Element of (pcs-reverse P); :: thesis:
assume that
A1: p = p' and
A2: q = q' ; :: thesis:
A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40;
assume A4: not [p',q'] in the ToleranceRel of (pcs-reverse P) ; :: according to PCS_0:def 7 :: thesis:
[p,q] in [:the carrier of P,the carrier of P:] by ZFMISC_1:106;
hence [p,q] in the ToleranceRel of P by A1, A2, A3, A4, XBOOLE_0:def 5; :: according to PCS_0:def 7 :: thesis: