theorem Th27: :: PCS_0:27

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