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_reflexive_in the carrier of P by Def9;
let x be object ; :: according to RELAT_2:def 2,PCS_0:def 10 :: thesis: ( not x in the carrier of (pcs-reverse P) or not [^,^] in the ToleranceRel of (pcs-reverse P) )
assume x in the carrier of (pcs-reverse P) ; :: thesis: not [^,^] in the ToleranceRel of (pcs-reverse P)
then [x,x] in the ToleranceRel of P by A1, A3;
hence not [^,^] in the ToleranceRel of (pcs-reverse P) by A2, XBOOLE_0:def 5; :: thesis: verum