theorem Th26: :: PCS_0:26

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 & p1 <= q1 holds
p <= q