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 object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: 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:105;
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 2;
then [p,p] in the InternalRel of P by A4;
hence [^,^] in the InternalRel of (pcs-extension (P,a)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;