set R = pcs-extension P,a;
A1: the carrier of (pcs-extension P,a) = {a} \/ the carrier of P by Def39;
A2: the ToleranceRel of (pcs-extension P,a) = ([:{a},the carrier of (pcs-extension P,a):] \/ [:the carrier of (pcs-extension P,a),{a}:]) \/ the ToleranceRel of P by Def39;
then A3: the ToleranceRel of (pcs-extension P,a) = [:{a},the carrier of (pcs-extension P,a):] \/ ([:the carrier of (pcs-extension P,a),{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4;
let p be set ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not p in the carrier of (pcs-extension P,a) or [^,^] in the ToleranceRel of (pcs-extension P,a) )
assume A4: p in the carrier of (pcs-extension P,a) ; :: thesis: [^,^] in the ToleranceRel of (pcs-extension P,a)

per cases ( p in {a} or p in the carrier of P ) by A1, A4, XBOOLE_0:def 3;

suppose p in {a} ; :: thesis: [^,^] in the ToleranceRel of (pcs-extension P,a)

then p = a by TARSKI:def 1;
then [p,p] in [:{a},the carrier of (pcs-extension P,a):] by A4, ZFMISC_1:128;
hence [^,^] in the ToleranceRel of (pcs-extension P,a) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A5: p in the carrier of P ; :: thesis: [^,^] in the ToleranceRel of (pcs-extension P,a)

the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
then [p,p] in the ToleranceRel of P by A5, RELAT_2:def 1;
hence [^,^] in the ToleranceRel of (pcs-extension P,a) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;