theorem Th38: :: PCS_0:38

for P, Q being non empty 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] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q by Def2;