let P be pcs; :: thesis: for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs
let a be set ; :: thesis: ( not a in the carrier of P implies pcs-extension (P,a) is pcs )
assume A1: not a in the carrier of P ; :: thesis: pcs-extension (P,a) is pcs
set R = pcs-extension (P,a);
( pcs-extension (P,a) is reflexive & pcs-extension (P,a) is transitive & pcs-extension (P,a) is pcs-tol-reflexive & pcs-extension (P,a) is pcs-tol-symmetric & pcs-extension (P,a) is pcs-compatible ) by A1, Th30, Th31;
hence pcs-extension (P,a) is pcs ; :: thesis: verum