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_irreflexive_in the carrier of P by Def10;
let x be object ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) )
assume A4: x in the carrier of (pcs-reverse P) ; :: thesis: [^,^] in the ToleranceRel of (pcs-reverse P)
then A5: not [x,x] in the ToleranceRel of P by A1, A3;
[x,x] in [: the carrier of (pcs-reverse P), the carrier of (pcs-reverse P):] by A4, ZFMISC_1:87;
hence [^,^] in the ToleranceRel of (pcs-reverse P) by A1, A2, A5, XBOOLE_0:def 5; :: thesis: verum