let P, Q be non empty 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] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
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] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
let p1, p2 be Element of P; :: thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
let q1, q2 be Element of Q; :: thesis: ( p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) implies p (--) q )
assume A1: ( p = [p1,q1] & q = [p2,q2] ) ; :: thesis: ( ( not p1 (--) p2 & not q1 (--) q2 ) or p (--) q )
assume ( p1 (--) p2 or q1 (--) q2 ) ; :: thesis: p (--) q
then ( [p1,p2] in the ToleranceRel of P or [q1,q2] in the ToleranceRel of Q ) by Def7;
hence [p,q] in the ToleranceRel of (P pcs-times Q) by A1, Def2; :: according to PCS_0:def 7 :: thesis: verum