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