set TR = the ToleranceRel of P;
A1: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
let x, y be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field the ToleranceRel of P or not y in field the ToleranceRel of P or not [^,^] in the ToleranceRel of P or [^,^] in the ToleranceRel of P )
assume that
x in field the ToleranceRel of P and
y in field the ToleranceRel of P ; :: thesis: ( not [^,^] in the ToleranceRel of P or [^,^] in the ToleranceRel of P )
assume A2: [x,y] in the ToleranceRel of P ; :: thesis: [^,^] in the ToleranceRel of P
then A3: x in dom the ToleranceRel of P by XTUPLE_0:def 12;
y in rng the ToleranceRel of P by A2, XTUPLE_0:def 13;
hence [^,^] in the ToleranceRel of P by A1, A2, A3; :: thesis: verum