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 ) } ;

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 ) }

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 ) }

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 A2, A5, A3, PROB_1:15, SETFAM_1:3;

for A being Subset of T st A is open holds

A in Y

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

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum

( 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

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 ) }
X c= 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 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;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

proof

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
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;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

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

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
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 ) }

end;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

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 A2, SETFAM_1:def 1; :: thesis: verumE ` 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 A4, SETFAM_1:def 1;

hence E ` in Z by PROB_1:def 1; :: thesis: verum

end;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 A4, SETFAM_1:def 1;

hence E ` in Z by PROB_1:def 1; :: thesis: verum

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 ) }

end;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

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 A2, SETFAM_1:def 1; :: thesis: verumIntersection 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 ;

S is SigmaField of T by A9, Th13;

hence Intersection BSeq in Z by A8, A10, PROB_1:def 6; :: thesis: verum

end;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

then A10:
rng BSeq c= Z
by NAT_1:52;let n be Nat; :: thesis: BSeq . n in Z

BSeq . n in rng BSeq by NAT_1:51;

hence BSeq . n in Z by A6, A7, SETFAM_1:def 1; :: thesis: verum

end;BSeq . n in rng BSeq by NAT_1:51;

hence BSeq . n in Z by A6, A7, SETFAM_1:def 1; :: thesis: verum

S is SigmaField of T by A9, Th13;

hence Intersection BSeq in Z by A8, A10, PROB_1:def 6; :: thesis: verum

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

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 A2, SETFAM_1:def 1;{} 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 {} 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 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 ) ;

then Z is Field_Subset of the carrier of T by Th13;

hence {} in Z by PROB_1:4; :: thesis: verum

end;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 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 ) ;

then Z is Field_Subset of the carrier of T by Th13;

hence {} in Z by PROB_1:4; :: thesis: verum

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 A2, A5, A3, PROB_1:15, SETFAM_1:3;

for A being Subset of T st A is open holds

A in Y

proof

then reconsider Y = Y as compl-closed all-open-containing closed_for_countable_unions Subset-Family of T by Def2;
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

end;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

hence
A in Y
by A2, SETFAM_1:def 1; :: thesis: verum
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 ex S being Subset-Family of the carrier of T st

( Y = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;

hence A in Y by A11, Def2; :: thesis: verum

end;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 ex S being Subset-Family of the carrier of T st

( Y = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;

hence A in Y by A11, Def2; :: thesis: verum

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

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
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 that

A12: X c= Z and

A13: Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ; :: thesis: Y c= Z

reconsider Z = Z as Subset-Family of T by A13;

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 A12, A13;

hence Y c= Z by SETFAM_1:3; :: thesis: verum

end;assume that

A12: X c= Z and

A13: Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ; :: thesis: Y c= Z

reconsider Z = Z as Subset-Family of T by A13;

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 A12, A13;

hence Y c= Z by SETFAM_1:3; :: thesis: verum

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum