set TR = the ToleranceRel of P;
A1: the ToleranceRel of P is_irreflexive_in the carrier of P by Def10;
let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field the ToleranceRel of P or not [^,^] in the ToleranceRel of P )
assume x in field the ToleranceRel of P ; :: thesis: not [^,^] in the ToleranceRel of P
assume A2: [x,x] in the ToleranceRel of P ; :: thesis: contradiction
then x in dom the ToleranceRel of P by XTUPLE_0:def 12;
hence contradiction by A1, A2; :: thesis: verum