let x be set ; :: 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;

now

let a, b be set ; :: thesis: ( a in x & b in x implies [a,b] in the ToleranceRel of P )
assume A3: ( a in x & b in x ) ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a1 = a, b1 = b as Element of P by A3;
a1 (--) b1 by A2, A3, Def43;
hence [a,b] in the ToleranceRel of P by Def7; :: thesis: verum

end;

hence [^,^] in the ToleranceRel of (pcs-general-power D) by A1, Def46; :: thesis: verum