set R = pcs-general-power D;
let x, y be object ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( not x in the carrier of (pcs-general-power D) or not y in the carrier of (pcs-general-power D) or not [^,^] in the ToleranceRel 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: ( not y in the carrier of (pcs-general-power D) or not [^,^] in the ToleranceRel of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) )
assume A2: y in the carrier of (pcs-general-power D) ; :: thesis: ( not [^,^] in the ToleranceRel of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) )
assume A3: [x,y] in the ToleranceRel of (pcs-general-power D) ; :: thesis: [^,^] in the ToleranceRel of (pcs-general-power D)
reconsider x = x, y = y as set by TARSKI:1;
now :: thesis: for a, b being set st a in y & b in x holds
[a,b] in the ToleranceRel of P
let a, b be set ; :: thesis: ( a in y & b in x implies [a,b] in the ToleranceRel of P )
assume that
A4: a in y and
A5: b in x ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a1 = a, b1 = b as Element of P by A1, A2, A4, A5;
[b,a] in the ToleranceRel of P by A3, A4, A5, Def46;
then b1 (--) a1 ;
hence [a,b] in the ToleranceRel of P by Def7; :: thesis: verum
end;
hence [^,^] in the ToleranceRel of (pcs-general-power D) by A1, A2, Def46; :: thesis: verum