set X = { B1 where B1 is Subset of P : B1 is B -omitting } ;
set O = the carrier of P;
{ B1 where B1 is Subset of P : B1 is B -omitting } c= bool the carrier of P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { B1 where B1 is Subset of P : B1 is B -omitting } or a in bool the carrier of P )
assume a in { B1 where B1 is Subset of P : B1 is B -omitting } ; :: thesis: a in bool the carrier of P
then consider B1 being Subset of P such that
A1: a = B1 and
B1 is B -omitting ;
thus a in bool the carrier of P by A1; :: thesis: verum

end;

hence { B1 where B1 is Subset of P : B1 is B -omitting } is Subset-Family of P ; :: thesis: verum