theorem Th34: :: PCS_0:34
for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds
not p9 (--) q9