let P, Q be pcs-Str ; :: thesis: for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds
q1 (--) q2
let p, q be Element of (P pcs-times Q); :: thesis: for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds
q1 (--) q2
let p1, p2 be Element of P; :: thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds
q1 (--) q2
let q1, q2 be Element of Q; :: thesis: ( p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 implies q1 (--) q2 )
assume that
A1: p = [p1,q1] and
A2: q = [p2,q2] ; :: thesis: ( not p (--) q or p1 (--) p2 or q1 (--) q2 )
assume p (--) q ; :: thesis: ( p1 (--) p2 or q1 (--) q2 )
then [p,q] in [^ the ToleranceRel of P, the ToleranceRel of Q^] ;
then consider a, b, c, d being set such that
A3: p = [a,b] and
A4: q = [c,d] and
a in the carrier of P and
b in the carrier of Q and
c in the carrier of P and
d in the carrier of Q and
A5: ( [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q ) by Def2;
A6: a = p1 by A1, A3, XTUPLE_0:1;
A7: b = q1 by A1, A3, XTUPLE_0:1;
A8: c = p2 by A2, A4, XTUPLE_0:1;
d = q2 by A2, A4, XTUPLE_0:1;
hence ( p1 (--) p2 or q1 (--) q2 ) by A5, A6, A7, A8; :: thesis: verum