let P, Q be pcs-Str ; :: thesis:
let p, q be Element of (P pcs-times Q); :: thesis:
let p1, p2 be Element of P; :: thesis:
let q1, q2 be Element of Q; :: thesis:
assume A1: ( p = [p1,q1] & q = [p2,q2] ) ; :: thesis:
assume p (--) q ; :: thesis:
then [p,q] in [^the ToleranceRel of P,the ToleranceRel of Q^] by Def7;
then consider a, b, c, d being set such that
A2: ( p = [a,b] & q = [c,d] ) and
( a in the carrier of P & b in the carrier of Q & c in the carrier of P & d in the carrier of Q ) and
A3: ( [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q ) by Def2;
( a = p1 & b = q1 & c = p2 & d = q2 ) by A1, A2, ZFMISC_1:33;
hence ( p1 (--) p2 or q1 (--) q2 ) by A3, Def7; :: thesis: