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 D2 = the carrier of Q as non empty set by A2;
reconsider TQ = the ToleranceRel of Q as Relation of D2 ;
D2 = field TQ by ORDERS_1:12;
then TQ is_reflexive_in D2 by RELAT_2:def 9;
then [x2,x2] in TQ by A2;
hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3, Def3; :: thesis: verum