set R = pcs-reverse P;
A1: the carrier of (pcs-reverse P) = the carrier of P by Def40;
A2: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40;
A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
let x, y be object ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( not x in the carrier of (pcs-reverse P) or not y in the carrier of (pcs-reverse P) or not [^,^] in the ToleranceRel of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) )
assume that
A4: x in the carrier of (pcs-reverse P) and
A5: y in the carrier of (pcs-reverse P) ; :: thesis: ( not [^,^] in the ToleranceRel of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) )
assume [x,y] in the ToleranceRel of (pcs-reverse P) ; :: thesis: [^,^] in the ToleranceRel of (pcs-reverse P)
then not [x,y] in the ToleranceRel of P by A2, XBOOLE_0:def 5;
then A6: not [y,x] in the ToleranceRel of P by A1, A3, A4, A5;
[y,x] in [: the carrier of P, the carrier of P:] by A1, A4, A5, ZFMISC_1:87;
hence [^,^] in the ToleranceRel of (pcs-reverse P) by A2, A6, XBOOLE_0:def 5; :: thesis: verum