let G be Subset-Family of P; :: thesis: ( G = Omit (P,B) iff for B1 being Subset of P holds
( B1 in G iff B1 is B -omitting ) )
set Om = Omit (P,B);
for B1 being Subset of P holds
( B1 in Omit (P,B) iff B1 is B -omitting )

proof

let B1 be Subset of P; :: thesis: ( B1 in Omit (P,B) iff B1 is B -omitting )
thus ( B1 in Omit (P,B) implies B1 is B -omitting ) :: thesis: ( B1 is B -omitting implies B1 in Omit (P,B) )

proof

assume B1 in Omit (P,B) ; :: thesis: B1 is B -omitting
then consider B2 being Subset of P such that
A5: ( B2 = B1 & B2 is B -omitting ) ;
thus B1 is B -omitting by A5; :: thesis: verum

end;

thus ( B1 is B -omitting implies B1 in Omit (P,B) ) ; :: thesis: verum

end;

hence ( G = Omit (P,B) implies for B1 being Subset of P holds
( B1 in G iff B1 is B -omitting ) ) ; :: thesis: ( ( for B1 being Subset of P holds
( B1 in G iff B1 is B -omitting ) ) implies G = Omit (P,B) )
assume A10: for B1 being Subset of P holds
( B1 in G iff B1 is B -omitting ) ; :: thesis: G = Omit (P,B)
thus G c= Omit (P,B) :: according to XBOOLE_0:def 10 :: thesis: Omit (P,B) c= G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in Omit (P,B) )
assume A11: a in G ; :: thesis: a in Omit (P,B)
then reconsider B1 = a as Subset of P ;
B1 is B -omitting by A10, A11;
hence a in Omit (P,B) ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Omit (P,B) or a in G )
assume a in Omit (P,B) ; :: thesis: a in G
then consider B1 being Subset of P such that
A21: ( B1 = a & B1 is B -omitting ) ;
thus a in G by A10, A21; :: thesis: verum