theorem Th35: :: PCS_0:35

for P being non empty pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds
p (--) q