set R = [^P,Q^];
set TR = the ToleranceRel of [^P,Q^];
A1: the ToleranceRel of [^P,Q^] is_symmetric_in field the ToleranceRel of [^P,Q^] by RELAT_2:def 11;
let x, y be object ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( not x in the carrier of [^P,Q^] or not y in the carrier of [^P,Q^] or not [^,^] in the ToleranceRel of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] )
assume that
x in the carrier of [^P,Q^] and
y in the carrier of [^P,Q^] ; :: thesis: ( not [^,^] in the ToleranceRel of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] )
assume A2: [x,y] in the ToleranceRel of [^P,Q^] ; :: thesis: [^,^] in the ToleranceRel of [^P,Q^]
then A3: x in field the ToleranceRel of [^P,Q^] by RELAT_1:15;
y in field the ToleranceRel of [^P,Q^] by A2, RELAT_1:15;
hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3; :: thesis: verum