set A = the Axioms of P;
set O = the carrier of P;
the carrier of P c= the carrier of P ;
then reconsider O = the carrier of P as Subset of P ;
take O ; :: thesis: O is inconsistent
for a being object st a in P \/ O holds
P \/ O |- a

proof

let a be object ; :: thesis: ( a in P \/ O implies P \/ O |- a )
assume a in P \/ O ; :: thesis: P \/ O |- a
then a in the Axioms of P \/ O by XBOOLE_1:12;
hence P \/ O |- a by Th46; :: thesis: verum

end;

then P \/ O is inconsistent ;
hence O is inconsistent ; :: thesis: verum