the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39;
hence not the carrier of (pcs-extension (P,a)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum