set B1 = the carrier of P;
the carrier of P c= the carrier of P ;
then reconsider B1 = the carrier of P as Subset of P ;
take B1 ; :: thesis: not B1 is B -omitting
for a being object st a in B holds
P \/ B1 |- a

proof

let a be object ; :: thesis: ( a in B implies P \/ B1 |- a )
assume A1: a in B ; :: thesis: P \/ B1 |- a
B1 = the Axioms of (P \/ B1) by XBOOLE_1:12;
hence P \/ B1 |- a by A1, Th46; :: thesis: verum

end;

hence not B1 is B -omitting ; :: thesis: verum