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 object ; :: 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:105;
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;
hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;