let x be object ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] )
assume x in the carrier of [^P,Q^] ; :: thesis: [^,^] in the ToleranceRel of [^P,Q^]
then consider x1, x2 being object such that
A1: x1 in the carrier of P and
A2: x2 in the carrier of Q and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider D1 = the carrier of P as non empty set by A1;
reconsider TP = the ToleranceRel of P as Relation of D1 ;
D1 = field TP by ORDERS_1:12;
then TP is_reflexive_in D1 by RELAT_2:def 9;
then [x1,x1] in TP by A1;
hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3, Def3; :: thesis: verum