set A = the Axioms of P;
set R = the Rules of P;
take E = {} the carrier of P; :: thesis: E is consistent
P is consistent ;
then consider a being object such that
A1: ( a in P & not P |- a ) ;
( a in P \/ E & not P \/ E |- a ) by A1;
then P \/ E is consistent ;
hence E is consistent ; :: thesis: verum