theorem Th31: :: PCS_0:31

for P being pcs-compatible pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible