set R = pcs-general-power D;
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of (pcs-general-power D) or [^,^] in the InternalRel of (pcs-general-power D) )
assume A1: x in the carrier of (pcs-general-power D) ; :: thesis: [^,^] in the InternalRel of (pcs-general-power D)
reconsider x = x as set by TARSKI:1;
for a being set st a in x holds
ex b being set st
( b in x & [a,b] in the InternalRel of P )
proof
let a be set ; :: thesis: ( a in x implies ex b being set st
( b in x & [a,b] in the InternalRel of P ) )
assume A2: a in x ; :: thesis: ex b being set st
( b in x & [a,b] in the InternalRel of P )
take a ; :: thesis: ( a in x & [a,a] in the InternalRel of P )
thus a in x by A2; :: thesis: [a,a] in the InternalRel of P
field the InternalRel of P = the carrier of P by ORDERS_1:12;
then the InternalRel of P is_reflexive_in the carrier of P by RELAT_2:def 9;
hence [a,a] in the InternalRel of P by A1, A2; :: thesis: verum
end;
hence [^,^] in the InternalRel of (pcs-general-power D) by A1, Def45; :: thesis: verum