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: now :: thesis: for Z being set st 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 ) } holds
X c= Z
end;
A2: 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;
A3: 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 A4: 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 :: thesis: for Z being set st 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 ) } holds
E ` in Z
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 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 ( E in Z & 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 ;
hence E ` in Z by 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 ; :: thesis: verum
end;
A5: 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 A6: 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 :: thesis: for Z being set st 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 ) } holds
Intersection BSeq in Z
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 A7: 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
A8: Z = S and
X c= S and
A9: S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ;
now :: thesis: for n being Nat holds BSeq . n in Z
let n be Nat; :: thesis: BSeq . n in Z
BSeq . n in rng BSeq by NAT_1:51;
hence BSeq . n in Z by ; :: thesis: verum
end;
then A10: rng BSeq c= Z by NAT_1:52;
S is SigmaField of T by ;
hence Intersection BSeq in Z by ; :: 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 ; :: thesis: verum
end;
now :: thesis: for Z being set st 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 ) } holds
{} in Z
end;
then {} 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 ;
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 ;
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 A11: 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 end;
hence A in Y by ; :: 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 ) )

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 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 ; :: thesis: verum