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

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

suppose p in {a} ; :: thesis: [^,^] in the InternalRel 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 A3, ZFMISC_1:128;
hence [^,^] in the InternalRel of (pcs-extension P,a) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;