theorem :: PCS_0:37

for P, Q being pcs-Str
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