theorem Th29: :: PCS_0:29

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q