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