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 A1: ( p = p' & q = q' ) ; :: thesis:
A2: ( the carrier of (pcs-reverse P) = the carrier of P & the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` ) by Def40;
assume A3: 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, XBOOLE_0:def 5; :: according to PCS_0:def 7 :: thesis: