let x be object ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) )
assume A1: x in the carrier of (pcs-general-power D) ; :: thesis: [^,^] in the ToleranceRel of (pcs-general-power D)
then reconsider x = x as Subset of P ;
A2: x is pcs-self-coherent by A1, Def44;
for a, b being set st a in x & b in x holds
[a,b] in the ToleranceRel of P by A2, Def7;
hence [^,^] in the ToleranceRel of (pcs-general-power D) by A1, Def46; :: thesis: verum