theorem Th25: :: PCS_0:25

for P being pcs-Str
for a being set
for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P