let T be non empty TopSpace; :: thesis: for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
let X be Subset-Family of T; :: thesis: ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
set V = { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
set Y = meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
A1: bool the carrier of T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }

proof

set X1 = TotFam T;
TotFam T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ;
hence bool the carrier of T in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: verum

end;

now

let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies {} in Z )
assume Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: {} in Z
then consider S being Subset-Family of T such that
A2: ( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
Z is Field_Subset of the carrier of T by A2, Th13;
hence {} in Z by PROB_1:10; :: thesis: verum

end;

then A3: {} in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A1, SETFAM_1:def 1;
A4: for BSeq being SetSequence of the carrier of T st rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }

proof

let BSeq be SetSequence of the carrier of T; :: thesis: ( rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } )
assume A5: rng BSeq c= meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }

now

let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies Intersection BSeq in Z )
assume A6: Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: Intersection BSeq in Z
then consider S being Subset-Family of T such that
A7: ( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
A8: ( Z = S & X c= S & S is SigmaField of T ) by A7, Th13;

now

let n be Nat; :: thesis: BSeq . n in Z
BSeq . n in rng BSeq by NAT_1:52;
then BSeq . n in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A5;
hence BSeq . n in Z by A6, SETFAM_1:def 1; :: thesis: verum

end;

then rng BSeq c= Z by NAT_1:53;
hence Intersection BSeq in Z by A8, PROB_1:def 8; :: thesis: verum

end;

hence Intersection BSeq in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A1, SETFAM_1:def 1; :: thesis: verum

end;

for E being Subset of T st E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }

proof

let E be Subset of T; :: thesis: ( E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } )
assume A9: E in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) }

now

let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies E ` in Z )
assume A10: Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: E ` in Z
then A11: E in Z by A9, SETFAM_1:def 1;
ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) by A10;
hence E ` in Z by A11, PROB_1:def 1; :: thesis: verum

end;

hence E ` in meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A1, SETFAM_1:def 1; :: thesis: verum

end;

then reconsider Y = meet { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } as SigmaField of T by A1, A3, A4, PROB_1:32, SETFAM_1:4;
for A being Subset of T st A is open holds
A in Y

proof

let A be Subset of T; :: thesis: ( A is open implies A in Y )
assume A12: A is open ; :: thesis: A in Y
for Y being set st Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } holds
A in Y

proof

let Y be set ; :: thesis: ( Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies A in Y )
assume Y in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: A in Y
then consider S being Subset-Family of the carrier of T such that
A13: ( Y = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
thus A in Y by A12, A13, Def2; :: thesis: verum

end;

hence A in Y by A1, SETFAM_1:def 1; :: thesis: verum

end;

then reconsider Y = Y as compl-closed all-open-containing closed_for_countable_unions Subset-Family of T by Def2;
take Y ; :: thesis: ( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )

A14: now

let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } implies X c= Z )
assume Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } ; :: thesis: X c= Z
then ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
hence X c= Z ; :: thesis: verum

end;

for Z being set st X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
Y c= Z

proof

let Z be set ; :: thesis: ( X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T implies Y c= Z )
assume A15: ( X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ; :: thesis: Y c= Z
then reconsider Z = Z as Subset-Family of T ;
Z in { S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) } by A15;
hence Y c= Z by SETFAM_1:4; :: thesis: verum

end;

hence ( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) ) by A1, A14, SETFAM_1:6; :: thesis: verum