:: TOPGEN_2 semantic presentation begin theorem Th1: :: TOPGEN_2:1 for T being non empty TopSpace for B being Basis of T for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x proof let T be non empty TopSpace; ::_thesis: for B being Basis of T for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x let B be Basis of T; ::_thesis: for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x let x be Element of T; ::_thesis: { U where U is Subset of T : ( x in U & U in B ) } is Basis of x set Bx = { U where U is Subset of T : ( x in U & U in B ) } ; A1: { U where U is Subset of T : ( x in U & U in B ) } c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B ) assume a in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in B then ex U being Subset of T st ( a = U & x in U & U in B ) ; hence a in B ; ::_thesis: verum end; then reconsider Bx = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1; Bx is Basis of x proof B c= the topology of T by TOPS_2:64; then Bx c= the topology of T by A1, XBOOLE_1:1; then A2: Bx is open by TOPS_2:64; Bx is x -quasi_basis proof now__::_thesis:_for_a_being_set_st_a_in_Bx_holds_ x_in_a let a be set ; ::_thesis: ( a in Bx implies x in a ) assume a in Bx ; ::_thesis: x in a then ex U being Subset of T st ( a = U & x in U & U in B ) ; hence x in a ; ::_thesis: verum end; hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K32( the carrier of T) holds ( not b1 is open or not x in b1 or ex b2 being Element of K32( the carrier of T) st ( b2 in Bx & b2 c= b1 ) ) let S be Subset of T; ::_thesis: ( not S is open or not x in S or ex b1 being Element of K32( the carrier of T) st ( b1 in Bx & b1 c= S ) ) assume that A3: S is open and A4: x in S ; ::_thesis: ex b1 being Element of K32( the carrier of T) st ( b1 in Bx & b1 c= S ) consider V being Subset of T such that A5: V in B and A6: x in V and A7: V c= S by A3, A4, YELLOW_9:31; V in Bx by A5, A6; hence ex b1 being Element of K32( the carrier of T) st ( b1 in Bx & b1 c= S ) by A7; ::_thesis: verum end; hence Bx is Basis of x by A2; ::_thesis: verum end; hence { U where U is Subset of T : ( x in U & U in B ) } is Basis of x ; ::_thesis: verum end; theorem Th2: :: TOPGEN_2:2 for T being non empty TopSpace for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds Union B is Basis of T proof let T be non empty TopSpace; ::_thesis: for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds Union B is Basis of T let B be ManySortedSet of T; ::_thesis: ( ( for x being Element of T holds B . x is Basis of x ) implies Union B is Basis of T ) assume A1: for x being Element of T holds B . x is Basis of x ; ::_thesis: Union B is Basis of T Union B c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Union B or a in bool the carrier of T ) assume a in Union B ; ::_thesis: a in bool the carrier of T then consider b being set such that A2: b in dom B and A3: a in B . b by CARD_5:2; reconsider b = b as Point of T by A2; B . b is Basis of b by A1; hence a in bool the carrier of T by A3; ::_thesis: verum end; then reconsider W = Union B as Subset-Family of T ; A4: dom B = the carrier of T by PARTFUN1:def_2; A5: now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ for_p_being_Point_of_T_st_p_in_A_holds_ ex_a_being_Subset_of_T_st_ (_a_in_W_&_p_in_a_&_a_c=_A_) let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in W & p in a & a c= A ) ) assume A6: A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in W & p in a & a c= A ) let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st ( a in W & p in a & a c= A ) ) assume A7: p in A ; ::_thesis: ex a being Subset of T st ( a in W & p in a & a c= A ) A8: B . p is Basis of p by A1; then consider a being Subset of T such that A9: a in B . p and A10: a c= A by A6, A7, YELLOW_8:def_1; take a = a; ::_thesis: ( a in W & p in a & a c= A ) thus a in W by A4, A9, CARD_5:2; ::_thesis: ( p in a & a c= A ) thus p in a by A8, A9, YELLOW_8:12; ::_thesis: a c= A thus a c= A by A10; ::_thesis: verum end; W c= the topology of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W or a in the topology of T ) assume a in W ; ::_thesis: a in the topology of T then consider b being set such that A11: b in dom B and A12: a in B . b by CARD_5:2; reconsider b = b as Point of T by A11; B . b is Basis of b by A1; then B . b c= the topology of T by TOPS_2:64; hence a in the topology of T by A12; ::_thesis: verum end; hence Union B is Basis of T by A5, YELLOW_9:32; ::_thesis: verum end; definition let T be non empty TopStruct ; let x be Element of T; func Chi (x,T) -> cardinal number means :Def1: :: TOPGEN_2:def 1 ( ex B being Basis of x st it = card B & ( for B being Basis of x holds it c= card B ) ); existence ex b1 being cardinal number st ( ex B being Basis of x st b1 = card B & ( for B being Basis of x holds b1 c= card B ) ) proof set B0 = the Basis of x; defpred S1[ ordinal number ] means ex B being Basis of x st \$1 = card B; card the Basis of x is ordinal ; then A1: ex A being ordinal number st S1[A] ; consider A being ordinal number such that A2: S1[A] and A3: for B being ordinal number st S1[B] holds A c= B from ORDINAL1:sch_1(A1); consider B1 being Basis of x such that A4: A = card B1 by A2; take card B1 ; ::_thesis: ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) ) thus ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) ) by A3, A4; ::_thesis: verum end; uniqueness for b1, b2 being cardinal number st ex B being Basis of x st b1 = card B & ( for B being Basis of x holds b1 c= card B ) & ex B being Basis of x st b2 = card B & ( for B being Basis of x holds b2 c= card B ) holds b1 = b2 proof let M1, M2 be cardinal number ; ::_thesis: ( ex B being Basis of x st M1 = card B & ( for B being Basis of x holds M1 c= card B ) & ex B being Basis of x st M2 = card B & ( for B being Basis of x holds M2 c= card B ) implies M1 = M2 ) assume that A5: ex B being Basis of x st M1 = card B and A6: for B being Basis of x holds M1 c= card B and A7: ex B being Basis of x st M2 = card B and A8: for B being Basis of x holds M2 c= card B ; ::_thesis: M1 = M2 thus ( M1 c= M2 & M2 c= M1 ) by A5, A6, A7, A8; :: according to XBOOLE_0:def_10 ::_thesis: verum end; end; :: deftheorem Def1 defines Chi TOPGEN_2:def_1_:_ for T being non empty TopStruct for x being Element of T for b3 being cardinal number holds ( b3 = Chi (x,T) iff ( ex B being Basis of x st b3 = card B & ( for B being Basis of x holds b3 c= card B ) ) ); theorem Th3: :: TOPGEN_2:3 for X being set st ( for a being set st a in X holds a is cardinal number ) holds union X is cardinal number proof let X be set ; ::_thesis: ( ( for a being set st a in X holds a is cardinal number ) implies union X is cardinal number ) assume A1: for a being set st a in X holds a is cardinal number ; ::_thesis: union X is cardinal number now__::_thesis:_for_a_being_set_st_a_in_X_holds_ ex_b_being_set_st_ (_b_in_X_&_a_c=_b_&_b_is_cardinal_set_) let a be set ; ::_thesis: ( a in X implies ex b being set st ( b in X & a c= b & b is cardinal set ) ) assume A2: a in X ; ::_thesis: ex b being set st ( b in X & a c= b & b is cardinal set ) then a is cardinal number by A1; hence ex b being set st ( b in X & a c= b & b is cardinal set ) by A2; ::_thesis: verum end; hence union X is cardinal number by CARD_LAR:32; ::_thesis: verum end; Lm1: now__::_thesis:_for_T_being_non_empty_TopStruct_holds_ (_union__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__is_cardinal_number_&_(_for_m_being_cardinal_number_st_m_=_union__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_ (_(_for_x_being_Point_of_T_holds_Chi_(x,T)_c=_m_)_&_(_for_M_being_cardinal_number_st_(_for_x_being_Point_of_T_holds_Chi_(x,T)_c=_M_)_holds_ m_c=_M_)_)_)_) let T be non empty TopStruct ; ::_thesis: ( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) ) ) set X = { (Chi (x,T)) where x is Point of T : verum } ; now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_ a_is_cardinal_number let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a is cardinal number ) assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a is cardinal number then ex x being Point of T st a = Chi (x,T) ; hence a is cardinal number ; ::_thesis: verum end; hence union { (Chi (x,T)) where x is Point of T : verum } is cardinal number by Th3; ::_thesis: for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) let m be cardinal number ; ::_thesis: ( m = union { (Chi (x,T)) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) ) assume A1: m = union { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) hereby ::_thesis: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M let x be Point of T; ::_thesis: Chi (x,T) c= m Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ; hence Chi (x,T) c= m by A1, ZFMISC_1:74; ::_thesis: verum end; let M be cardinal number ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= M ) implies m c= M ) assume A2: for x being Point of T holds Chi (x,T) c= M ; ::_thesis: m c= M now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_ a_c=_M let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= M ) assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a c= M then ex x being Point of T st a = Chi (x,T) ; hence a c= M by A2; ::_thesis: verum end; hence m c= M by A1, ZFMISC_1:76; ::_thesis: verum end; definition let T be non empty TopStruct ; func Chi T -> cardinal number means :Def2: :: TOPGEN_2:def 2 ( ( for x being Point of T holds Chi (x,T) c= it ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds it c= M ) ); existence ex b1 being cardinal number st ( ( for x being Point of T holds Chi (x,T) c= b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds b1 c= M ) ) proof set X = { (Chi (x,T)) where x is Point of T : verum } ; reconsider m = union { (Chi (x,T)) where x is Point of T : verum } as cardinal number by Lm1; take m ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) thus ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being cardinal number st ( for x being Point of T holds Chi (x,T) c= b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds b1 c= M ) & ( for x being Point of T holds Chi (x,T) c= b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds b2 c= M ) holds b1 = b2 proof let M1, M2 be cardinal number ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= M1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds M1 c= M ) & ( for x being Point of T holds Chi (x,T) c= M2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds M2 c= M ) implies M1 = M2 ) assume that A1: for x being Point of T holds Chi (x,T) c= M1 and A2: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds M1 c= M and A3: for x being Point of T holds Chi (x,T) c= M2 and A4: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds M2 c= M ; ::_thesis: M1 = M2 thus ( M1 c= M2 & M2 c= M1 ) by A1, A2, A3, A4; :: according to XBOOLE_0:def_10 ::_thesis: verum end; end; :: deftheorem Def2 defines Chi TOPGEN_2:def_2_:_ for T being non empty TopStruct for b2 being cardinal number holds ( b2 = Chi T iff ( ( for x being Point of T holds Chi (x,T) c= b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds b2 c= M ) ) ); theorem Th4: :: TOPGEN_2:4 for T being non empty TopStruct holds Chi T = union { (Chi (x,T)) where x is Point of T : verum } proof let T be non empty TopStruct ; ::_thesis: Chi T = union { (Chi (x,T)) where x is Point of T : verum } set X = { (Chi (x,T)) where x is Point of T : verum } ; reconsider m = union { (Chi (x,T)) where x is Point of T : verum } as cardinal number by Lm1; A1: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds m c= M by Lm1; for x being Point of T holds Chi (x,T) c= m by Lm1; hence Chi T = union { (Chi (x,T)) where x is Point of T : verum } by A1, Def2; ::_thesis: verum end; theorem Th5: :: TOPGEN_2:5 for T being non empty TopStruct for x being Point of T holds Chi (x,T) c= Chi T proof let T be non empty TopStruct ; ::_thesis: for x being Point of T holds Chi (x,T) c= Chi T set X = { (Chi (x,T)) where x is Point of T : verum } ; let x be Point of T; ::_thesis: Chi (x,T) c= Chi T A1: Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ; Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4; hence Chi (x,T) c= Chi T by A1, ZFMISC_1:74; ::_thesis: verum end; theorem :: TOPGEN_2:6 for T being non empty TopSpace holds ( T is first-countable iff Chi T c= omega ) proof let T be non empty TopSpace; ::_thesis: ( T is first-countable iff Chi T c= omega ) set X = { (Chi (x,T)) where x is Point of T : verum } ; A1: Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4; thus ( T is first-countable implies Chi T c= omega ) ::_thesis: ( Chi T c= omega implies T is first-countable ) proof assume A2: for x being Point of T ex B being Basis of x st B is countable ; :: according to FRECHET:def_2 ::_thesis: Chi T c= omega now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_ a_c=_omega let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= omega ) assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a c= omega then consider x being Point of T such that A3: a = Chi (x,T) ; consider B being Basis of x such that A4: B is countable by A2; A5: card B c= omega by A4, CARD_3:def_14; Chi (x,T) c= card B by Def1; hence a c= omega by A3, A5, XBOOLE_1:1; ::_thesis: verum end; hence Chi T c= omega by A1, ZFMISC_1:76; ::_thesis: verum end; assume A6: Chi T c= omega ; ::_thesis: T is first-countable let x be Point of T; :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of K32(K32( the carrier of T)) st b1 is countable consider B being Basis of x such that A7: Chi (x,T) = card B by Def1; take B ; ::_thesis: B is countable Chi (x,T) c= Chi T by Th5; hence card B c= omega by A6, A7, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum end; begin definition let T be non empty TopSpace; mode Neighborhood_System of T -> ManySortedSet of T means :Def3: :: TOPGEN_2:def 3 for x being Element of T holds it . x is Basis of x; existence ex b1 being ManySortedSet of T st for x being Element of T holds b1 . x is Basis of x proof set B = the Basis of T; deffunc H1( Point of T) -> set = { U where U is Subset of T : ( \$1 in U & U in the Basis of T ) } ; consider F being ManySortedSet of T such that A1: for x being Point of T holds F . x = H1(x) from PBOOLE:sch_5(); take F ; ::_thesis: for x being Element of T holds F . x is Basis of x let x be Point of T; ::_thesis: F . x is Basis of x F . x = H1(x) by A1; hence F . x is Basis of x by Th1; ::_thesis: verum end; end; :: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def_3_:_ for T being non empty TopSpace for b2 being ManySortedSet of T holds ( b2 is Neighborhood_System of T iff for x being Element of T holds b2 . x is Basis of x ); definition let T be non empty TopSpace; let N be Neighborhood_System of T; :: original: Union redefine func Union N -> Basis of T; coherence Union N is Basis of T proof for x being Point of T holds N . x is Basis of x by Def3; hence Union N is Basis of T by Th2; ::_thesis: verum end; let x be Point of T; :: original: . redefine funcN . x -> Basis of x; coherence N . x is Basis of x by Def3; end; theorem :: TOPGEN_2:7 for T being non empty TopSpace for x, y being Point of T for B1 being Basis of x for B2 being Basis of y for U being set st x in U & U in B2 holds ex V being open Subset of T st ( V in B1 & V c= U ) proof let T be non empty TopSpace; ::_thesis: for x, y being Point of T for B1 being Basis of x for B2 being Basis of y for U being set st x in U & U in B2 holds ex V being open Subset of T st ( V in B1 & V c= U ) let x, y be Point of T; ::_thesis: for B1 being Basis of x for B2 being Basis of y for U being set st x in U & U in B2 holds ex V being open Subset of T st ( V in B1 & V c= U ) let B1 be Basis of x; ::_thesis: for B2 being Basis of y for U being set st x in U & U in B2 holds ex V being open Subset of T st ( V in B1 & V c= U ) let B2 be Basis of y; ::_thesis: for U being set st x in U & U in B2 holds ex V being open Subset of T st ( V in B1 & V c= U ) let U be set ; ::_thesis: ( x in U & U in B2 implies ex V being open Subset of T st ( V in B1 & V c= U ) ) assume that A1: x in U and A2: U in B2 ; ::_thesis: ex V being open Subset of T st ( V in B1 & V c= U ) U is open Subset of T by A2, YELLOW_8:12; then consider V being Subset of T such that A3: V in B1 and A4: V c= U by A1, YELLOW_8:13; V is open by A3, YELLOW_8:12; hence ex V being open Subset of T st ( V in B1 & V c= U ) by A3, A4; ::_thesis: verum end; theorem :: TOPGEN_2:8 for T being non empty TopSpace for x being Point of T for B being Basis of x for U1, U2 being set st U1 in B & U2 in B holds ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) proof let T be non empty TopSpace; ::_thesis: for x being Point of T for B being Basis of x for U1, U2 being set st U1 in B & U2 in B holds ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) let x be Point of T; ::_thesis: for B being Basis of x for U1, U2 being set st U1 in B & U2 in B holds ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) let B be Basis of x; ::_thesis: for U1, U2 being set st U1 in B & U2 in B holds ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) let U1, U2 be set ; ::_thesis: ( U1 in B & U2 in B implies ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) ) assume that A1: U1 in B and A2: U2 in B ; ::_thesis: ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) reconsider U1 = U1, U2 = U2 as open Subset of T by A1, A2, YELLOW_8:12; A3: x in U2 by A2, YELLOW_8:12; x in U1 by A1, YELLOW_8:12; then x in U1 /\ U2 by A3, XBOOLE_0:def_4; then consider V being Subset of T such that A4: V in B and A5: V c= U1 /\ U2 by YELLOW_8:13; V is open by A4, YELLOW_8:12; hence ex V being open Subset of T st ( V in B & V c= U1 /\ U2 ) by A4, A5; ::_thesis: verum end; Lm2: now__::_thesis:_for_T_being_non_empty_TopSpace for_A_being_Subset_of_T for_x_being_Element_of_T_st_x_in_Cl_A_holds_ for_B_being_Basis_of_x for_U_being_set_st_U_in_B_holds_ U_meets_A let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Element of T st x in Cl A holds for B being Basis of x for U being set st U in B holds U meets A let A be Subset of T; ::_thesis: for x being Element of T st x in Cl A holds for B being Basis of x for U being set st U in B holds U meets A let x be Element of T; ::_thesis: ( x in Cl A implies for B being Basis of x for U being set st U in B holds U meets A ) assume A1: x in Cl A ; ::_thesis: for B being Basis of x for U being set st U in B holds U meets A let B be Basis of x; ::_thesis: for U being set st U in B holds U meets A let U be set ; ::_thesis: ( U in B implies U meets A ) assume A2: U in B ; ::_thesis: U meets A then x in U by YELLOW_8:12; then U meets Cl A by A1, XBOOLE_0:3; hence U meets A by A2, TSEP_1:36, YELLOW_8:12; ::_thesis: verum end; Lm3: now__::_thesis:_for_T_being_non_empty_TopSpace for_A_being_Subset_of_T for_x_being_Element_of_T_st_ex_B_being_Basis_of_x_st_ for_U_being_set_st_U_in_B_holds_ U_meets_A_holds_ x_in_Cl_A let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Element of T st ex B being Basis of x st for U being set st U in B holds U meets A holds x in Cl A let A be Subset of T; ::_thesis: for x being Element of T st ex B being Basis of x st for U being set st U in B holds U meets A holds x in Cl A let x be Element of T; ::_thesis: ( ex B being Basis of x st for U being set st U in B holds U meets A implies x in Cl A ) given B being Basis of x such that A1: for U being set st U in B holds U meets A ; ::_thesis: x in Cl A now__::_thesis:_for_U_being_Subset_of_T_st_U_is_open_&_x_in_U_holds_ A_meets_U let U be Subset of T; ::_thesis: ( U is open & x in U implies A meets U ) assume that A2: U is open and A3: x in U ; ::_thesis: A meets U ex V being Subset of T st ( V in B & V c= U ) by A2, A3, YELLOW_8:def_1; hence A meets U by A1, XBOOLE_1:63; ::_thesis: verum end; hence x in Cl A by PRE_TOPC:def_7; ::_thesis: verum end; theorem :: TOPGEN_2:9 for T being non empty TopSpace for A being Subset of T for x being Element of T holds ( x in Cl A iff for B being Basis of x for U being set st U in B holds U meets A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Element of T holds ( x in Cl A iff for B being Basis of x for U being set st U in B holds U meets A ) let A be Subset of T; ::_thesis: for x being Element of T holds ( x in Cl A iff for B being Basis of x for U being set st U in B holds U meets A ) let x be Element of T; ::_thesis: ( x in Cl A iff for B being Basis of x for U being set st U in B holds U meets A ) set B = the Basis of x; thus ( x in Cl A implies for B being Basis of x for U being set st U in B holds U meets A ) by Lm2; ::_thesis: ( ( for B being Basis of x for U being set st U in B holds U meets A ) implies x in Cl A ) assume for B being Basis of x for U being set st U in B holds U meets A ; ::_thesis: x in Cl A then for U being set st U in the Basis of x holds U meets A ; hence x in Cl A by Lm3; ::_thesis: verum end; theorem :: TOPGEN_2:10 for T being non empty TopSpace for A being Subset of T for x being Element of T holds ( x in Cl A iff ex B being Basis of x st for U being set st U in B holds U meets A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Element of T holds ( x in Cl A iff ex B being Basis of x st for U being set st U in B holds U meets A ) let A be Subset of T; ::_thesis: for x being Element of T holds ( x in Cl A iff ex B being Basis of x st for U being set st U in B holds U meets A ) let x be Element of T; ::_thesis: ( x in Cl A iff ex B being Basis of x st for U being set st U in B holds U meets A ) set B = the Basis of x; ( x in Cl A implies for U being set st U in the Basis of x holds U meets A ) by Lm2; hence ( x in Cl A implies ex B being Basis of x st for U being set st U in B holds U meets A ) ; ::_thesis: ( ex B being Basis of x st for U being set st U in B holds U meets A implies x in Cl A ) thus ( ex B being Basis of x st for U being set st U in B holds U meets A implies x in Cl A ) by Lm3; ::_thesis: verum end; registration let T be TopSpace; cluster non empty open for Element of K32(K32( the carrier of T)); existence ex b1 being Subset-Family of T st ( b1 is open & not b1 is empty ) proof take the topology of T ; ::_thesis: ( the topology of T is open & not the topology of T is empty ) thus ( the topology of T is open & not the topology of T is empty ) ; ::_thesis: verum end; end; begin theorem Th11: :: TOPGEN_2:11 for T being non empty TopSpace for S being open Subset-Family of T ex G being open Subset-Family of T st ( G c= S & union G = union S & card G c= weight T ) proof defpred S1[ set , set ] means \$1 c= \$2; let T be non empty TopSpace; ::_thesis: for S being open Subset-Family of T ex G being open Subset-Family of T st ( G c= S & union G = union S & card G c= weight T ) let S be open Subset-Family of T; ::_thesis: ex G being open Subset-Family of T st ( G c= S & union G = union S & card G c= weight T ) consider B being Basis of T such that A1: card B = weight T by WAYBEL23:74; set B1 = { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } ; { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } or a in B ) assume a in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } ; ::_thesis: a in B then ex W being Subset of T st ( a = W & W in B & ex U being set st ( U in S & W c= U ) ) ; hence a in B ; ::_thesis: verum end; then A2: card { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } c= card B by CARD_1:11; A3: now__::_thesis:_for_a_being_set_st_a_in__{__W_where_W_is_Subset_of_T_:_(_W_in_B_&_ex_U_being_set_st_ (_U_in_S_&_W_c=_U_)_)__}__holds_ ex_b_being_set_st_ (_b_in_S_&_S1[a,b]_) let a be set ; ::_thesis: ( a in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } implies ex b being set st ( b in S & S1[a,b] ) ) assume a in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } ; ::_thesis: ex b being set st ( b in S & S1[a,b] ) then ex W being Subset of T st ( a = W & W in B & ex U being set st ( U in S & W c= U ) ) ; hence ex b being set st ( b in S & S1[a,b] ) ; ::_thesis: verum end; consider f being Function such that A4: ( dom f = { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } & rng f c= S ) and A5: for a being set st a in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } holds S1[a,f . a] from FUNCT_1:sch_5(A3); set G = rng f; reconsider G = rng f as open Subset-Family of T by A4, TOPS_2:11, XBOOLE_1:1; take G ; ::_thesis: ( G c= S & union G = union S & card G c= weight T ) thus ( G c= S & union G c= union S ) by A4, ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: ( union S c= union G & card G c= weight T ) thus union S c= union G ::_thesis: card G c= weight T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union S or a in union G ) assume a in union S ; ::_thesis: a in union G then consider b being set such that A6: a in b and A7: b in S by TARSKI:def_4; reconsider b = b as open Subset of T by A7, TOPS_2:def_1; reconsider a = a as Point of T by A6, A7; consider W0 being Subset of T such that A8: W0 in B and A9: a in W0 and A10: W0 c= b by A6, YELLOW_9:31; A11: W0 in { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } by A7, A8, A10; then f . W0 in G by A4, FUNCT_1:def_3; then A12: f . W0 c= union G by ZFMISC_1:74; W0 c= f . W0 by A5, A11; then a in f . W0 by A9; hence a in union G by A12; ::_thesis: verum end; card G c= card { W where W is Subset of T : ( W in B & ex U being set st ( U in S & W c= U ) ) } by A4, CARD_1:12; hence card G c= weight T by A1, A2, XBOOLE_1:1; ::_thesis: verum end; definition let T be TopStruct ; attrT is finite-weight means :Def4: :: TOPGEN_2:def 4 weight T is finite ; end; :: deftheorem Def4 defines finite-weight TOPGEN_2:def_4_:_ for T being TopStruct holds ( T is finite-weight iff weight T is finite ); notation let T be TopStruct ; antonym infinite-weight T for finite-weight ; end; registration cluster finite -> finite-weight for TopStruct ; coherence for b1 being TopStruct st b1 is finite holds b1 is finite-weight proof let T be TopStruct ; ::_thesis: ( T is finite implies T is finite-weight ) assume A1: the carrier of T is finite ; :: according to STRUCT_0:def_11 ::_thesis: T is finite-weight ex B being Basis of T st card B = weight T by WAYBEL23:74; hence weight T is finite by A1; :: according to TOPGEN_2:def_4 ::_thesis: verum end; cluster infinite-weight -> infinite for TopStruct ; coherence for b1 being TopStruct st b1 is infinite-weight holds b1 is infinite ; end; theorem Th12: :: TOPGEN_2:12 for X being set holds card (SmallestPartition X) = card X proof let X be set ; ::_thesis: card (SmallestPartition X) = card X set A = SmallestPartition X; percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: card (SmallestPartition X) = card X hence card (SmallestPartition X) = card X by EQREL_1:32; ::_thesis: verum end; suppose X <> {} ; ::_thesis: card (SmallestPartition X) = card X then reconsider X = X as non empty set ; deffunc H1( set ) -> set = {\$1}; A1: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37; then A2: for a being set st a in X holds H1(a) in SmallestPartition X ; consider f being Function of X,(SmallestPartition X) such that A3: for a being set st a in X holds f . a = H1(a) from FUNCT_2:sch_2(A2); A4: rng f = SmallestPartition X proof thus rng f c= SmallestPartition X ; :: according to XBOOLE_0:def_10 ::_thesis: SmallestPartition X c= rng f let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition X or a in rng f ) assume a in SmallestPartition X ; ::_thesis: a in rng f then consider b being Element of X such that A5: a = {b} by A1; f . b = a by A3, A5; hence a in rng f by FUNCT_2:4; ::_thesis: verum end; A6: f is one-to-one proof let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not a in proj1 f or not b1 in proj1 f or not f . a = f . b1 or a = b1 ) let b be set ; ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b ) assume that A7: a in dom f and A8: b in dom f ; ::_thesis: ( not f . a = f . b or a = b ) assume f . a = f . b ; ::_thesis: a = b then {a} = f . b by A3, A7 .= {b} by A3, A8 ; hence a = b by ZFMISC_1:3; ::_thesis: verum end; dom f = X by FUNCT_2:def_1; then X, SmallestPartition X are_equipotent by A4, A6, WELLORD2:def_4; hence card (SmallestPartition X) = card X by CARD_1:5; ::_thesis: verum end; end; end; theorem Th13: :: TOPGEN_2:13 for T being non empty discrete TopStruct holds ( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) ) proof let T be non empty discrete TopStruct ; ::_thesis: ( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) ) set B0 = SmallestPartition the carrier of T; A1: SmallestPartition the carrier of T c= the topology of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition the carrier of T or a in the topology of T ) assume a in SmallestPartition the carrier of T ; ::_thesis: a in the topology of T then reconsider a = a as Subset of T ; a is open by TDLAT_3:15; hence a in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; A2: SmallestPartition the carrier of T = { {a} where a is Element of T : verum } by EQREL_1:37; now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ for_p_being_Point_of_T_st_p_in_A_holds_ ex_a_being_Subset_of_T_st_ (_a_in_SmallestPartition_the_carrier_of_T_&_p_in_a_&_a_c=_A_) let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in SmallestPartition the carrier of T & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in SmallestPartition the carrier of T & p in a & a c= A ) let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st ( a in SmallestPartition the carrier of T & p in a & a c= A ) ) assume A3: p in A ; ::_thesis: ex a being Subset of T st ( a in SmallestPartition the carrier of T & p in a & a c= A ) reconsider a = {p} as Subset of T ; take a = a; ::_thesis: ( a in SmallestPartition the carrier of T & p in a & a c= A ) thus a in SmallestPartition the carrier of T by A2; ::_thesis: ( p in a & a c= A ) thus p in a by TARSKI:def_1; ::_thesis: a c= A thus a c= A by A3, ZFMISC_1:31; ::_thesis: verum end; hence A4: SmallestPartition the carrier of T is Basis of T by A1, YELLOW_9:32; ::_thesis: for B being Basis of T holds SmallestPartition the carrier of T c= B let B be Basis of T; ::_thesis: SmallestPartition the carrier of T c= B let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition the carrier of T or a in B ) assume A5: a in SmallestPartition the carrier of T ; ::_thesis: a in B then consider b being Element of T such that A6: a = {b} by A2; reconsider a = a as Subset of T by A5; A7: b in a by A6, TARSKI:def_1; a is open by A4, A5, YELLOW_8:10; then consider U being Subset of T such that A8: U in B and A9: b in U and A10: U c= a by A7, YELLOW_9:31; a c= U by A6, A9, ZFMISC_1:31; hence a in B by A8, A10, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th14: :: TOPGEN_2:14 for T being non empty discrete TopStruct holds weight T = card the carrier of T proof let T be non empty discrete TopStruct ; ::_thesis: weight T = card the carrier of T set M = { (card C) where C is Basis of T : verum } ; reconsider B0 = SmallestPartition the carrier of T as Basis of T by Th13; A1: card B0 in { (card C) where C is Basis of T : verum } ; A2: card B0 = card the carrier of T by Th12; weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def_5; hence weight T c= card the carrier of T by A2, A1, SETFAM_1:3; :: according to XBOOLE_0:def_10 ::_thesis: card the carrier of T c= weight T ex B being Basis of T st card B = weight T by WAYBEL23:74; hence card the carrier of T c= weight T by A2, Th13, CARD_1:11; ::_thesis: verum end; registration cluster TopSpace-like infinite-weight for TopStruct ; existence ex b1 being TopSpace st b1 is infinite-weight proof set A = the infinite set ; reconsider O = bool the infinite set as Subset-Family of the infinite set ; reconsider T = TopStruct(# the infinite set ,O #) as non empty discrete TopStruct by TDLAT_3:def_1; take T ; ::_thesis: T is infinite-weight weight T = card the carrier of T by Th14; hence weight T is infinite ; :: according to TOPGEN_2:def_4 ::_thesis: verum end; end; Lm4: for T being infinite-weight TopSpace for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) proof let T be infinite-weight TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) let B be Basis of T; ::_thesis: ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) consider B0 being Basis of T such that A1: card B0 = weight T by WAYBEL23:74; defpred S1[ set , set ] means ( union \$2 = \$1 & card \$2 c= weight T ); A2: now__::_thesis:_for_a_being_set_st_a_in_B0_holds_ ex_b_being_set_st_ (_b_in_bool_B_&_S1[a,b]_) let a be set ; ::_thesis: ( a in B0 implies ex b being set st ( b in bool B & S1[a,b] ) ) set Sa = { U where U is Subset of T : ( U in B & U c= a ) } ; A3: { U where U is Subset of T : ( U in B & U c= a ) } c= B proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { U where U is Subset of T : ( U in B & U c= a ) } or b in B ) assume b in { U where U is Subset of T : ( U in B & U c= a ) } ; ::_thesis: b in B then ex U being Subset of T st ( b = U & U in B & U c= a ) ; hence b in B ; ::_thesis: verum end; assume a in B0 ; ::_thesis: ex b being set st ( b in bool B & S1[a,b] ) then reconsider W = a as open Subset of T by YELLOW_8:10; A4: union { U where U is Subset of T : ( U in B & U c= a ) } = W by YELLOW_8:9; reconsider Sa = { U where U is Subset of T : ( U in B & U c= a ) } as open Subset-Family of T by A3, TOPS_2:11, XBOOLE_1:1; consider G being open Subset-Family of T such that A5: G c= Sa and A6: union G = union Sa and A7: card G c= weight T by Th11; reconsider b = G as set ; take b = b; ::_thesis: ( b in bool B & S1[a,b] ) b c= B by A3, A5, XBOOLE_1:1; hence b in bool B ; ::_thesis: S1[a,b] thus S1[a,b] by A4, A6, A7; ::_thesis: verum end; consider f being Function such that A8: ( dom f = B0 & rng f c= bool B ) and A9: for a being set st a in B0 holds S1[a,f . a] from FUNCT_1:sch_5(A2); A10: Union f c= union (bool B) by A8, ZFMISC_1:77; then A11: Union f c= B by ZFMISC_1:81; then reconsider B1 = Union f as Subset-Family of T by XBOOLE_1:1; now__::_thesis:_(_B1_c=_the_topology_of_T_&_(_for_A_being_Subset_of_T_st_A_is_open_holds_ for_p_being_Point_of_T_st_p_in_A_holds_ ex_a_being_Subset_of_T_st_ (_a_in_B1_&_p_in_a_&_a_c=_A_)_)_) B c= the topology of T by TOPS_2:64; hence B1 c= the topology of T by A11, XBOOLE_1:1; ::_thesis: for A being Subset of T st A is open holds for p being Point of T st p in A holds ex a being Subset of T st ( a in B1 & p in a & a c= A ) let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in B1 & p in a & a c= A ) ) assume A12: A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in B1 & p in a & a c= A ) let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st ( a in B1 & p in a & a c= A ) ) assume p in A ; ::_thesis: ex a being Subset of T st ( a in B1 & p in a & a c= A ) then consider U being Subset of T such that A13: U in B0 and A14: p in U and A15: U c= A by A12, YELLOW_9:31; A16: S1[U,f . U] by A9, A13; then consider a being set such that A17: p in a and A18: a in f . U by A14, TARSKI:def_4; A19: a c= U by A16, A18, ZFMISC_1:74; a in B1 by A8, A13, A18, CARD_5:2; hence ex a being Subset of T st ( a in B1 & p in a & a c= A ) by A15, A17, A19, XBOOLE_1:1; ::_thesis: verum end; then reconsider B1 = B1 as Basis of T by YELLOW_9:32; now__::_thesis:_(_card_(rng_f)_c=_weight_T_&_(_for_a_being_set_st_a_in_rng_f_holds_ card_a_c=_weight_T_)_) thus card (rng f) c= weight T by A1, A8, CARD_1:12; ::_thesis: for a being set st a in rng f holds card a c= weight T let a be set ; ::_thesis: ( a in rng f implies card a c= weight T ) assume a in rng f ; ::_thesis: card a c= weight T then ex b being set st ( b in dom f & a = f . b ) by FUNCT_1:def_3; hence card a c= weight T by A8, A9; ::_thesis: verum end; then A20: card B1 c= (weight T) *` (weight T) by CARD_2:87; take B1 ; ::_thesis: ( B1 c= B & card B1 = weight T ) thus B1 c= B by A10, ZFMISC_1:81; ::_thesis: card B1 = weight T weight T is infinite by Def4; hence card B1 c= weight T by A20, CARD_4:15; :: according to XBOOLE_0:def_10 ::_thesis: weight T c= card B1 thus weight T c= card B1 by WAYBEL23:73; ::_thesis: verum end; theorem Th15: :: TOPGEN_2:15 for T being non empty finite-weight TopSpace ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) ) proof let T be non empty finite-weight TopSpace; ::_thesis: ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) ) consider B being Basis of T such that A1: card B = weight T by WAYBEL23:74; deffunc H1( set ) -> set = meet { U where U is Subset of T : ( \$1 in U & U in B ) } ; A2: B is finite by A1, Def4; A3: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_T_holds_ H1(a)_in_the_topology_of_T B c= the topology of T by TOPS_2:64; then FinMeetCl B c= FinMeetCl the topology of T by CANTOR_1:14; then A4: FinMeetCl B c= the topology of T by CANTOR_1:5; let a be set ; ::_thesis: ( a in the carrier of T implies H1(a) in the topology of T ) assume a in the carrier of T ; ::_thesis: H1(a) in the topology of T then reconsider x = a as Point of T ; set S = { U where U is Subset of T : ( x in U & U in B ) } ; consider U being Subset of T such that A5: U in B and A6: x in U and U c= [#] T by YELLOW_9:31; A7: { U where U is Subset of T : ( x in U & U in B ) } c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B ) assume a in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in B then ex U being Subset of T st ( a = U & x in U & U in B ) ; hence a in B ; ::_thesis: verum end; then reconsider S = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1; Intersect S in FinMeetCl B by A2, A7, CANTOR_1:def_3; then A8: Intersect S in the topology of T by A4; U in S by A5, A6; hence H1(a) in the topology of T by A8, SETFAM_1:def_9; ::_thesis: verum end; consider f being Function of the carrier of T, the topology of T such that A9: for a being set st a in the carrier of T holds f . a = H1(a) from FUNCT_2:sch_2(A3); set B0 = rng f; reconsider B0 = rng f as Subset-Family of T by XBOOLE_1:1; A10: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_T_holds_ a_in_f_._a let a be set ; ::_thesis: ( a in the carrier of T implies a in f . a ) assume a in the carrier of T ; ::_thesis: a in f . a then reconsider x = a as Point of T ; set S = { U where U is Subset of T : ( x in U & U in B ) } ; consider U being Subset of T such that A11: U in B and A12: x in U and U c= [#] T by YELLOW_9:31; A13: now__::_thesis:_for_b_being_set_st_b_in__{__U_where_U_is_Subset_of_T_:_(_x_in_U_&_U_in_B_)__}__holds_ a_in_b let b be set ; ::_thesis: ( b in { U where U is Subset of T : ( x in U & U in B ) } implies a in b ) assume b in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in b then ex U being Subset of T st ( b = U & a in U & U in B ) ; hence a in b ; ::_thesis: verum end; A14: f . a = meet { U where U is Subset of T : ( x in U & U in B ) } by A9; U in { U where U is Subset of T : ( x in U & U in B ) } by A11, A12; hence a in f . a by A14, A13, SETFAM_1:def_1; ::_thesis: verum end; A15: now__::_thesis:_for_x_being_Point_of_T for_V_being_Subset_of_T_st_x_in_V_&_V_is_open_holds_ f_._x_c=_V let x be Point of T; ::_thesis: for V being Subset of T st x in V & V is open holds f . x c= V let V be Subset of T; ::_thesis: ( x in V & V is open implies f . x c= V ) set S = { U where U is Subset of T : ( x in U & U in B ) } ; assume that A16: x in V and A17: V is open ; ::_thesis: f . x c= V consider U being Subset of T such that A18: U in B and A19: x in U and A20: U c= V by A16, A17, YELLOW_9:31; A21: f . x = meet { U where U is Subset of T : ( x in U & U in B ) } by A9; U in { U where U is Subset of T : ( x in U & U in B ) } by A18, A19; then f . x c= U by A21, SETFAM_1:3; hence f . x c= V by A20, XBOOLE_1:1; ::_thesis: verum end; now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ for_p_being_Point_of_T_st_p_in_A_holds_ ex_a_being_Subset_of_T_st_ (_a_in_B0_&_p_in_a_&_a_c=_A_) let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in B0 & p in a & a c= A ) ) assume A22: A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in B0 & p in a & a c= A ) let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st ( a in B0 & p in a & a c= A ) ) assume A23: p in A ; ::_thesis: ex a being Subset of T st ( a in B0 & p in a & a c= A ) f . p in the topology of T ; then reconsider a = f . p as Subset of T ; take a = a; ::_thesis: ( a in B0 & p in a & a c= A ) thus a in B0 by FUNCT_2:4; ::_thesis: ( p in a & a c= A ) thus p in a by A10; ::_thesis: a c= A thus a c= A by A15, A22, A23; ::_thesis: verum end; then reconsider B0 = B0 as Basis of T by YELLOW_9:32; take B0 ; ::_thesis: ex f being Function of the carrier of T, the topology of T st ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) ) take f ; ::_thesis: ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) ) thus B0 = rng f ; ::_thesis: for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) let x be Point of T; ::_thesis: ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) thus ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) by A10, A15; ::_thesis: verum end; theorem Th16: :: TOPGEN_2:16 for T being TopSpace for B0, B being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds B0 c= B proof let T be TopSpace; ::_thesis: for B0, B being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds B0 c= B let B0, B be Basis of T; ::_thesis: for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds B0 c= B let f be Function of the carrier of T, the topology of T; ::_thesis: ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) implies B0 c= B ) assume A1: B0 = rng f ; ::_thesis: ( ex x being Point of T st ( x in f . x implies ex U being open Subset of T st ( x in U & not f . x c= U ) ) or B0 c= B ) assume A2: for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ; ::_thesis: B0 c= B let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B0 or a in B ) assume A3: a in B0 ; ::_thesis: a in B then reconsider V = a as Subset of T ; consider b being set such that A4: b in dom f and A5: a = f . b by A1, A3, FUNCT_1:def_3; A6: V is open by A3, YELLOW_8:10; reconsider b = b as Element of T by A4; b in V by A2, A5; then consider U being Subset of T such that A7: U in B and A8: b in U and A9: U c= V by A6, YELLOW_9:31; U is open by A7, YELLOW_8:10; then a c= U by A2, A5, A8; hence a in B by A7, A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th17: :: TOPGEN_2:17 for T being TopSpace for B0 being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds weight T = card B0 proof let T be TopSpace; ::_thesis: for B0 being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds weight T = card B0 let B0 be Basis of T; ::_thesis: for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) holds weight T = card B0 let f be Function of the carrier of T, the topology of T; ::_thesis: ( B0 = rng f & ( for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ) implies weight T = card B0 ) assume that A1: B0 = rng f and A2: for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) ; ::_thesis: weight T = card B0 set M = { (card C) where C is Basis of T : verum } ; A3: card B0 in { (card C) where C is Basis of T : verum } ; weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def_5; hence weight T c= card B0 by A3, SETFAM_1:3; :: according to XBOOLE_0:def_10 ::_thesis: card B0 c= weight T ex B being Basis of T st card B = weight T by WAYBEL23:74; hence card B0 c= weight T by A1, A2, Th16, CARD_1:11; ::_thesis: verum end; Lm5: for T being non empty finite-weight TopSpace for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) proof let T be non empty finite-weight TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) let B be Basis of T; ::_thesis: ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) consider B0 being Basis of T, f being Function of the carrier of T, the topology of T such that A1: B0 = rng f and A2: for x being Point of T holds ( x in f . x & ( for U being open Subset of T st x in U holds f . x c= U ) ) by Th15; take B0 ; ::_thesis: ( B0 c= B & card B0 = weight T ) thus B0 c= B by A1, A2, Th16; ::_thesis: card B0 = weight T thus card B0 c= weight T by A1, A2, Th17; :: according to XBOOLE_0:def_10 ::_thesis: weight T c= card B0 thus weight T c= card B0 by WAYBEL23:73; ::_thesis: verum end; theorem :: TOPGEN_2:18 for T being non empty TopSpace for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) proof let T be non empty TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) let B be Basis of T; ::_thesis: ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) ( T is finite-weight or T is infinite-weight ) ; hence ex B1 being Basis of T st ( B1 c= B & card B1 = weight T ) by Lm4, Lm5; ::_thesis: verum end; begin definition let X, x0 be set ; func DiscrWithInfin (X,x0) -> strict TopStruct means :Def5: :: TOPGEN_2:def 5 ( the carrier of it = X & the topology of it = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ); uniqueness for b1, b2 being strict TopStruct st the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } & the carrier of b2 = X & the topology of b2 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } holds b1 = b2 ; existence ex b1 being strict TopStruct st ( the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) proof set O1 = { U where U is Subset of X : not x0 in U } ; set O2 = { (F `) where F is Subset of X : F is finite } ; set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ; { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } c= bool X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } or a in bool X ) assume a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in bool X then ( a in { U where U is Subset of X : not x0 in U } or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def_3; then ( ex U being Subset of X st ( a = U & not x0 in U ) or ex F being Subset of X st ( a = F ` & F is finite ) ) ; hence a in bool X ; ::_thesis: verum end; then reconsider O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of X ; take TopStruct(# X,O #) ; ::_thesis: ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) thus ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def_5_:_ for X, x0 being set for b3 being strict TopStruct holds ( b3 = DiscrWithInfin (X,x0) iff ( the carrier of b3 = X & the topology of b3 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) ); registration let X, x0 be set ; cluster DiscrWithInfin (X,x0) -> strict TopSpace-like ; coherence DiscrWithInfin (X,x0) is TopSpace-like proof set O1 = { U where U is Subset of X : not x0 in U } ; set O2 = { (F `) where F is Subset of X : F is finite } ; set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ; set T = DiscrWithInfin (X,x0); A1: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; A2: the topology of (DiscrWithInfin (X,x0)) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } by Def5; ({} X) ` = X ; then X in { (F `) where F is Subset of X : F is finite } ; hence the carrier of (DiscrWithInfin (X,x0)) in the topology of (DiscrWithInfin (X,x0)) by A1, A2, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K32(K32( the carrier of (DiscrWithInfin (X,x0)))) holds ( not b1 c= the topology of (DiscrWithInfin (X,x0)) or union b1 in the topology of (DiscrWithInfin (X,x0)) ) ) & ( for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds ( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) ) ) ) hereby ::_thesis: for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds ( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) ) let a be Subset-Family of (DiscrWithInfin (X,x0)); ::_thesis: ( a c= the topology of (DiscrWithInfin (X,x0)) implies union b1 in the topology of (DiscrWithInfin (X,x0)) ) assume A3: a c= the topology of (DiscrWithInfin (X,x0)) ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0)) percases ( not a c= { U where U is Subset of X : not x0 in U } or a c= { U where U is Subset of X : not x0 in U } ) ; suppose not a c= { U where U is Subset of X : not x0 in U } ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0)) then consider b being set such that A4: b in a and A5: not b in { U where U is Subset of X : not x0 in U } by TARSKI:def_3; b in { (F `) where F is Subset of X : F is finite } by A2, A3, A4, A5, XBOOLE_0:def_3; then A6: ex F being Subset of X st ( b = F ` & F is finite ) ; A7: ((union a) `) ` = union a ; b c= union a by A4, ZFMISC_1:74; then (union a) ` is finite by A1, A6, FINSET_1:1, SUBSET_1:17; then union a in { (F `) where F is Subset of X : F is finite } by A1, A7; hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; supposeA8: a c= { U where U is Subset of X : not x0 in U } ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0)) now__::_thesis:_not_x0_in_union_a assume x0 in union a ; ::_thesis: contradiction then consider b being set such that A9: x0 in b and A10: b in a by TARSKI:def_4; b in { U where U is Subset of X : not x0 in U } by A8, A10; then ex U being Subset of X st ( b = U & not x0 in U ) ; hence contradiction by A9; ::_thesis: verum end; then union a in { U where U is Subset of X : not x0 in U } by A1; hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; end; end; let a, b be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( not a in the topology of (DiscrWithInfin (X,x0)) or not b in the topology of (DiscrWithInfin (X,x0)) or a /\ b in the topology of (DiscrWithInfin (X,x0)) ) assume that A11: a in the topology of (DiscrWithInfin (X,x0)) and A12: b in the topology of (DiscrWithInfin (X,x0)) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0)) percases ( ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) or a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) by A2, A11, A12, XBOOLE_0:def_3; supposeA13: ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0)) then consider F2 being Subset of X such that A14: b = F2 ` and A15: F2 is finite ; consider F1 being Subset of X such that A16: a = F1 ` and A17: F1 is finite by A13; a /\ b = (F1 \/ F2) ` by A16, A14, XBOOLE_1:53; then a /\ b in { (F `) where F is Subset of X : F is finite } by A17, A15; hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; suppose ( a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0)) then ( ex U being Subset of X st ( a = U & not x0 in U ) or ex U being Subset of X st ( b = U & not x0 in U ) ) ; then not x0 in a /\ b by XBOOLE_0:def_4; then a /\ b in { U where U is Subset of X : not x0 in U } by A1; hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; registration let X be non empty set ; let x0 be set ; cluster DiscrWithInfin (X,x0) -> non empty strict ; coherence not DiscrWithInfin (X,x0) is empty by Def5; end; theorem Th19: :: TOPGEN_2:19 for X, x0 being set for A being Subset of (DiscrWithInfin (X,x0)) holds ( A is open iff ( not x0 in A or A ` is finite ) ) proof let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds ( A is open iff ( not x0 in A or A ` is finite ) ) set T = DiscrWithInfin (X,x0); set O1 = { U where U is Subset of X : not x0 in U } ; set O2 = { (F `) where F is Subset of X : F is finite } ; let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is open iff ( not x0 in A or A ` is finite ) ) A1: the topology of (DiscrWithInfin (X,x0)) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } by Def5; A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; thus ( not A is open or not x0 in A or A ` is finite ) ::_thesis: ( ( not x0 in A or A ` is finite ) implies A is open ) proof assume A in the topology of (DiscrWithInfin (X,x0)) ; :: according to PRE_TOPC:def_2 ::_thesis: ( not x0 in A or A ` is finite ) then ( A in { U where U is Subset of X : not x0 in U } or A in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def_3; then ( ex U being Subset of X st ( A = U & not x0 in U ) or ex F being Subset of X st ( A = F ` & F is finite ) ) ; hence ( not x0 in A or A ` is finite ) by A2; ::_thesis: verum end; assume ( not x0 in A or A ` is finite ) ; ::_thesis: A is open then ( A in { U where U is Subset of X : not x0 in U } or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A2; hence A in the topology of (DiscrWithInfin (X,x0)) by A1, XBOOLE_0:def_3; :: according to PRE_TOPC:def_2 ::_thesis: verum end; theorem Th20: :: TOPGEN_2:20 for X, x0 being set for A being Subset of (DiscrWithInfin (X,x0)) holds ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) proof let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) set T = DiscrWithInfin (X,x0); let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) ( A is closed iff A ` is open ) by TOPS_1:3; then A1: ( A is closed iff ( not x0 in A ` or (A `) ` is finite ) ) by Th19; the carrier of (DiscrWithInfin (X,x0)) = X by Def5; hence ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: TOPGEN_2:21 for X, x0, x being set st x in X holds {x} is closed Subset of (DiscrWithInfin (X,x0)) proof let X, x0, x be set ; ::_thesis: ( x in X implies {x} is closed Subset of (DiscrWithInfin (X,x0)) ) set T = DiscrWithInfin (X,x0); the carrier of (DiscrWithInfin (X,x0)) = X by Def5; hence ( x in X implies {x} is closed Subset of (DiscrWithInfin (X,x0)) ) by Th20, ZFMISC_1:31; ::_thesis: verum end; theorem Th22: :: TOPGEN_2:22 for X, x0, x being set st x in X & x <> x0 holds {x} is open Subset of (DiscrWithInfin (X,x0)) proof let X, x0, x be set ; ::_thesis: ( x in X & x <> x0 implies {x} is open Subset of (DiscrWithInfin (X,x0)) ) set T = DiscrWithInfin (X,x0); assume that A1: x in X and A2: x <> x0 ; ::_thesis: {x} is open Subset of (DiscrWithInfin (X,x0)) A3: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; not x0 in {x} by A2, TARSKI:def_1; hence {x} is open Subset of (DiscrWithInfin (X,x0)) by A3, A1, Th19, ZFMISC_1:31; ::_thesis: verum end; theorem :: TOPGEN_2:23 for X, x0 being set st X is infinite holds for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds not U is open proof let X, x0 be set ; ::_thesis: ( X is infinite implies for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds not U is open ) set T = DiscrWithInfin (X,x0); assume A1: X is infinite ; ::_thesis: for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds not U is open let U be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( U = {x0} implies not U is open ) assume A2: U = {x0} ; ::_thesis: not U is open the carrier of (DiscrWithInfin (X,x0)) = X by Def5; then X = (U `) \/ {x0} by A2, XBOOLE_1:45; then A3: U ` is infinite by A1; x0 in U by A2, TARSKI:def_1; hence not U is open by A3, Th19; ::_thesis: verum end; theorem Th24: :: TOPGEN_2:24 for X, x0 being set for A being Subset of (DiscrWithInfin (X,x0)) st A is finite holds Cl A = A proof let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is finite holds Cl A = A let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is finite implies Cl A = A ) assume A is finite ; ::_thesis: Cl A = A then A is closed by Th20; hence Cl A = A by PRE_TOPC:22; ::_thesis: verum end; theorem Th25: :: TOPGEN_2:25 for T being non empty TopSpace for A being Subset of T st not A is closed holds for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a} proof let T be non empty TopSpace; ::_thesis: for A being Subset of T st not A is closed holds for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a} let A be Subset of T; ::_thesis: ( not A is closed implies for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a} ) assume A1: not A is closed ; ::_thesis: for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a} A2: A c= Cl A by PRE_TOPC:18; let a be Point of T; ::_thesis: ( A \/ {a} is closed implies Cl A = A \/ {a} ) assume A \/ {a} is closed ; ::_thesis: Cl A = A \/ {a} then A3: Cl (A \/ {a}) = A \/ {a} by PRE_TOPC:22; Cl A c= Cl (A \/ {a}) by PRE_TOPC:19, XBOOLE_1:7; hence Cl A = A \/ {a} by A1, A2, A3, ZFMISC_1:138; ::_thesis: verum end; theorem Th26: :: TOPGEN_2:26 for X, x0 being set st x0 in X holds for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds Cl A = A \/ {x0} proof let X, x0 be set ; ::_thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds Cl A = A \/ {x0} ) assume A1: x0 in X ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds Cl A = A \/ {x0} set T = DiscrWithInfin (X,x0); reconsider T = DiscrWithInfin (X,x0) as non empty TopSpace by A1; reconsider x = x0 as Point of T by A1, Def5; let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is infinite implies Cl A = A \/ {x0} ) reconsider B = {x} as Subset of T ; reconsider A9 = A as Subset of T ; x0 in {x0} by TARSKI:def_1; then x0 in A9 \/ B by XBOOLE_0:def_3; then A9 \/ B is closed by Th20; then A2: Cl (A9 \/ B) = A9 \/ B by PRE_TOPC:22; assume A is infinite ; ::_thesis: Cl A = A \/ {x0} then ( not A9 is closed or x0 in A ) by A1, Th20; hence Cl A = A \/ {x0} by A2, Th25, ZFMISC_1:40; ::_thesis: verum end; theorem :: TOPGEN_2:27 for X, x0 being set for A being Subset of (DiscrWithInfin (X,x0)) st A ` is finite holds Int A = A proof let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A ` is finite holds Int A = A let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A ` is finite implies Int A = A ) assume A ` is finite ; ::_thesis: Int A = A then Cl (A `) = A ` by Th24; hence Int A = (A `) ` by TOPS_1:def_1 .= A ; ::_thesis: verum end; theorem :: TOPGEN_2:28 for X, x0 being set st x0 in X holds for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds Int A = A \ {x0} proof let X, x0 be set ; ::_thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds Int A = A \ {x0} ) assume A1: x0 in X ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds Int A = A \ {x0} set T = DiscrWithInfin (X,x0); reconsider T = DiscrWithInfin (X,x0) as non empty TopSpace by A1; reconsider x = x0 as Point of T by A1, Def5; let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A ` is infinite implies Int A = A \ {x0} ) reconsider A9 = A as Subset of T ; assume A ` is infinite ; ::_thesis: Int A = A \ {x0} then Cl (A `) = (A9 `) \/ {x} by A1, Th26; hence Int A = ((A9 `) \/ {x}) ` by TOPS_1:def_1 .= ((A9 \ {x}) `) ` by SUBSET_1:14 .= A \ {x0} ; ::_thesis: verum end; theorem Th29: :: TOPGEN_2:29 for X, x0 being set ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } proof let X, x0 be set ; ::_thesis: ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } set T = DiscrWithInfin (X,x0); set B1 = (SmallestPartition X) \ {{x0}}; set B2 = { (F `) where F is Subset of X : F is finite } ; A1: (SmallestPartition X) \ {{x0}} c= the topology of (DiscrWithInfin (X,x0)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in the topology of (DiscrWithInfin (X,x0)) ) assume A2: a in (SmallestPartition X) \ {{x0}} ; ::_thesis: a in the topology of (DiscrWithInfin (X,x0)) then A3: a in SmallestPartition X by ZFMISC_1:56; then reconsider X = X as non empty set by EQREL_1:32; SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37; then A4: ex x being Element of X st a = {x} by A3; a <> {x0} by A2, ZFMISC_1:56; then not x0 in a by A4, TARSKI:def_1; then a is open Subset of (DiscrWithInfin (X,x0)) by A2, Def5, Th19; hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def_2; ::_thesis: verum end; A5: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; { (F `) where F is Subset of X : F is finite } c= bool the carrier of (DiscrWithInfin (X,x0)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in bool the carrier of (DiscrWithInfin (X,x0)) ) assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in bool the carrier of (DiscrWithInfin (X,x0)) then ex F being Subset of X st ( a = F ` & F is finite ) ; hence a in bool the carrier of (DiscrWithInfin (X,x0)) by A5; ::_thesis: verum end; then reconsider B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of (DiscrWithInfin (X,x0)) by A5, XBOOLE_1:8; A6: now__::_thesis:_for_A_being_Subset_of_(DiscrWithInfin_(X,x0))_st_A_is_open_holds_ for_p_being_Point_of_(DiscrWithInfin_(X,x0))_st_p_in_A_holds_ ex_a_being_Subset_of_(DiscrWithInfin_(X,x0))_st_ (_a_in_B0_&_p_in_a_&_a_c=_A_) let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is open implies for p being Point of (DiscrWithInfin (X,x0)) st p in A holds ex a being Subset of (DiscrWithInfin (X,x0)) st ( a in B0 & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of (DiscrWithInfin (X,x0)) st p in A holds ex a being Subset of (DiscrWithInfin (X,x0)) st ( a in B0 & p in a & a c= A ) then A7: ( not x0 in A or A ` is finite ) by Th19; let p be Point of (DiscrWithInfin (X,x0)); ::_thesis: ( p in A implies ex a being Subset of (DiscrWithInfin (X,x0)) st ( a in B0 & p in a & a c= A ) ) assume A8: p in A ; ::_thesis: ex a being Subset of (DiscrWithInfin (X,x0)) st ( a in B0 & p in a & a c= A ) reconsider X9 = X as non empty set by A8, Def5; reconsider p9 = p as Element of X9 by Def5; SmallestPartition X = { {x} where x is Element of X9 : verum } by EQREL_1:37; then A9: {p9} in SmallestPartition X ; ( {p} <> {x0} or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A5, A8, A7, ZFMISC_1:3; then ( not {p} in {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by TARSKI:def_1; then ( {p} in (SmallestPartition X) \ {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by A9, XBOOLE_0:def_5; then ( ( {p} in B0 & p in {p} & {p} c= A ) or ( A in B0 & A c= A ) ) by A8, XBOOLE_0:def_3, ZFMISC_1:31; hence ex a being Subset of (DiscrWithInfin (X,x0)) st ( a in B0 & p in a & a c= A ) by A8; ::_thesis: verum end; { (F `) where F is Subset of X : F is finite } c= the topology of (DiscrWithInfin (X,x0)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in the topology of (DiscrWithInfin (X,x0)) ) assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in the topology of (DiscrWithInfin (X,x0)) then consider F being Subset of X such that A10: a = F ` and A11: F is finite ; (F `) ` is finite by A11; then a is open Subset of (DiscrWithInfin (X,x0)) by A5, A10, Th19; hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def_2; ::_thesis: verum end; then reconsider B0 = B0 as Basis of (DiscrWithInfin (X,x0)) by A1, A6, XBOOLE_1:8, YELLOW_9:32; take B0 ; ::_thesis: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } thus B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: verum end; theorem :: TOPGEN_2:30 for X being infinite set holds card (Fin X) = card X proof deffunc H1( set ) -> set = proj2 \$1; let X be infinite set ; ::_thesis: card (Fin X) = card X set FX = Fin X; consider f being Function such that A1: ( dom f = X * & ( for a being set st a in X * holds f . a = H1(a) ) ) from FUNCT_1:sch_3(); Fin X c= rng f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Fin X or a in rng f ) assume A2: a in Fin X ; ::_thesis: a in rng f then a is finite by FINSUB_1:def_5; then consider p being FinSequence such that A3: a = rng p by FINSEQ_1:52; a c= X by A2, FINSUB_1:def_5; then p is FinSequence of X by A3, FINSEQ_1:def_4; then A4: p in X * by FINSEQ_1:def_11; then f . p in rng f by A1, FUNCT_1:def_3; hence a in rng f by A1, A3, A4; ::_thesis: verum end; then card (Fin X) c= card (X *) by A1, CARD_1:12; hence card (Fin X) c= card X by CARD_4:24; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card (Fin X) set SX = SmallestPartition X; SmallestPartition X c= Fin X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition X or a in Fin X ) assume a in SmallestPartition X ; ::_thesis: a in Fin X then a in { {x} where x is Element of X : verum } by EQREL_1:37; then ex x being Element of X st a = {x} ; hence a in Fin X by FINSUB_1:def_5; ::_thesis: verum end; then card (SmallestPartition X) c= card (Fin X) by CARD_1:11; hence card X c= card (Fin X) by Th12; ::_thesis: verum end; theorem Th31: :: TOPGEN_2:31 for X being infinite set holds card { (F `) where F is Subset of X : F is finite } = card X proof let X be infinite set ; ::_thesis: card { (F `) where F is Subset of X : F is finite } = card X set FX = { (F `) where F is Subset of X : F is finite } ; deffunc H1( set ) -> Element of K32(X) = X \ (proj2 \$1); consider f being Function such that A1: ( dom f = X * & ( for a being set st a in X * holds f . a = H1(a) ) ) from FUNCT_1:sch_3(); { (F `) where F is Subset of X : F is finite } c= rng f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in rng f ) assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in rng f then consider F being Subset of X such that A2: a = F ` and A3: F is finite ; consider p being FinSequence such that A4: F = rng p by A3, FINSEQ_1:52; p is FinSequence of X by A4, FINSEQ_1:def_4; then A5: p in X * by FINSEQ_1:def_11; then f . p in rng f by A1, FUNCT_1:def_3; hence a in rng f by A1, A2, A4, A5; ::_thesis: verum end; then card { (F `) where F is Subset of X : F is finite } c= card (X *) by A1, CARD_1:12; hence card { (F `) where F is Subset of X : F is finite } c= card X by CARD_4:24; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card { (F `) where F is Subset of X : F is finite } deffunc H2( set ) -> Element of K32(X) = X \ {\$1}; consider f being Function such that A6: ( dom f = X & ( for a being set st a in X holds f . a = H2(a) ) ) from FUNCT_1:sch_3(); A7: rng f c= { (F `) where F is Subset of X : F is finite } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in { (F `) where F is Subset of X : F is finite } ) assume a in rng f ; ::_thesis: a in { (F `) where F is Subset of X : F is finite } then consider b being set such that A8: b in dom f and A9: a = f . b by FUNCT_1:def_3; reconsider b = b as Element of X by A6, A8; {b} ` in { (F `) where F is Subset of X : F is finite } ; hence a in { (F `) where F is Subset of X : F is finite } by A6, A9; ::_thesis: verum end; f is one-to-one proof let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not a in proj1 f or not b1 in proj1 f or not f . a = f . b1 or a = b1 ) let b be set ; ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b ) assume that A10: a in dom f and A11: b in dom f and A12: f . a = f . b ; ::_thesis: a = b reconsider a = a, b = b as Element of X by A6, A10, A11; {a} ` = f . b by A6, A12 .= {b} ` by A6 ; then {a} = {b} by SUBSET_1:42; hence a = b by ZFMISC_1:3; ::_thesis: verum end; hence card X c= card { (F `) where F is Subset of X : F is finite } by A6, A7, CARD_1:10; ::_thesis: verum end; theorem Th32: :: TOPGEN_2:32 for X being infinite set for x0 being set for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds card B0 = card X proof let X be infinite set ; ::_thesis: for x0 being set for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds card B0 = card X let x0 be set ; ::_thesis: for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds card B0 = card X set T = DiscrWithInfin (X,x0); let B0 be Basis of (DiscrWithInfin (X,x0)); ::_thesis: ( B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } implies card B0 = card X ) set SX = SmallestPartition X; set FX = { (F `) where F is Subset of X : F is finite } ; assume A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: card B0 = card X A2: card (SmallestPartition X) = card X by Th12; A3: card {{x0}} = 1 by CARD_1:30; A4: 1 in card X by CARD_3:86; then (card X) +` 1 = card X by CARD_2:76; then A5: card ((SmallestPartition X) \ {{x0}}) = card X by A3, A2, A4, CARD_2:98; card { (F `) where F is Subset of X : F is finite } = card X by Th31; then card B0 c= (card X) +` (card X) by A1, A5, CARD_2:34; hence card B0 c= card X by CARD_2:75; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card B0 thus card X c= card B0 by A1, A5, CARD_1:11, XBOOLE_1:7; ::_thesis: verum end; theorem Th33: :: TOPGEN_2:33 for X being infinite set for x0 being set for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B proof let X be infinite set ; ::_thesis: for x0 being set for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B let x0 be set ; ::_thesis: for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B set T = DiscrWithInfin (X,x0); set SX = SmallestPartition X; A1: card {{x0}} = 1 by CARD_1:30; A2: card (SmallestPartition X) = card X by Th12; let B be Basis of (DiscrWithInfin (X,x0)); ::_thesis: card X c= card B A3: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; A4: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37; A5: (SmallestPartition X) \ {{x0}} c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in B ) assume A6: a in (SmallestPartition X) \ {{x0}} ; ::_thesis: a in B then not a in {{x0}} by XBOOLE_0:def_5; then A7: a <> {x0} by TARSKI:def_1; a in SmallestPartition X by A6, XBOOLE_0:def_5; then ex x being Element of X st a = {x} by A4; then consider x being Element of (DiscrWithInfin (X,x0)) such that A8: a = {x} and A9: x <> x0 by A3, A7; A10: x in a by A8, TARSKI:def_1; a is open Subset of (DiscrWithInfin (X,x0)) by A3, A8, A9, Th22; then consider U being Subset of (DiscrWithInfin (X,x0)) such that A11: U in B and A12: x in U and A13: U c= a by A10, YELLOW_9:31; a c= U by A8, A12, ZFMISC_1:31; hence a in B by A11, A13, XBOOLE_0:def_10; ::_thesis: verum end; A14: 1 in card X by CARD_3:86; then (card X) +` 1 = card X by CARD_2:76; then card ((SmallestPartition X) \ {{x0}}) = card X by A1, A2, A14, CARD_2:98; hence card X c= card B by A5, CARD_1:11; ::_thesis: verum end; theorem :: TOPGEN_2:34 for X being infinite set for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X proof let X be infinite set ; ::_thesis: for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X let x0 be set ; ::_thesis: weight (DiscrWithInfin (X,x0)) = card X set T = DiscrWithInfin (X,x0); consider B0 being Basis of (DiscrWithInfin (X,x0)) such that A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29; card B0 = card X by A1, Th32; hence weight (DiscrWithInfin (X,x0)) c= card X by WAYBEL23:73; :: according to XBOOLE_0:def_10 ::_thesis: card X c= weight (DiscrWithInfin (X,x0)) ex B being Basis of (DiscrWithInfin (X,x0)) st card B = weight (DiscrWithInfin (X,x0)) by WAYBEL23:74; hence card X c= weight (DiscrWithInfin (X,x0)) by Th33; ::_thesis: verum end; theorem :: TOPGEN_2:35 for X being non empty set for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } proof let X be non empty set ; ::_thesis: for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } let x0 be set ; ::_thesis: ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } set T = DiscrWithInfin (X,x0); set SX = SmallestPartition X; set FX = { (F `) where F is Subset of X : F is finite } ; set AX = { ({x} `) where x is Element of X : verum } ; reconsider SX = SmallestPartition X as Subset-Family of (DiscrWithInfin (X,x0)) by Def5; { ({x} `) where x is Element of X : verum } c= bool X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ({x} `) where x is Element of X : verum } or a in bool X ) assume a in { ({x} `) where x is Element of X : verum } ; ::_thesis: a in bool X then ex x being Element of X st a = {x} ` ; hence a in bool X ; ::_thesis: verum end; then reconsider AX = { ({x} `) where x is Element of X : verum } as Subset-Family of (DiscrWithInfin (X,x0)) by Def5; reconsider pB = (SX \ {{x0}}) \/ AX as Subset-Family of (DiscrWithInfin (X,x0)) ; consider B0 being Basis of (DiscrWithInfin (X,x0)) such that A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29; A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5; A3: { (F `) where F is Subset of X : F is finite } c= FinMeetCl pB proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in FinMeetCl pB ) assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in FinMeetCl pB then consider F being Subset of (DiscrWithInfin (X,x0)) such that A4: a = F ` and A5: F is finite by A2; set SF = SmallestPartition F; bool F c= bool X by A2, ZFMISC_1:67; then reconsider SF = SmallestPartition F as Subset-Family of (DiscrWithInfin (X,x0)) by A2, XBOOLE_1:1; percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: a in FinMeetCl pB hence a in FinMeetCl pB by A4, CANTOR_1:8; ::_thesis: verum end; suppose F <> {} ; ::_thesis: a in FinMeetCl pB then reconsider F = F as non empty Subset of (DiscrWithInfin (X,x0)) ; SF is a_partition of F ; then reconsider SF = SF as non empty Subset-Family of (DiscrWithInfin (X,x0)) ; A6: COMPLEMENT SF c= pB proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in COMPLEMENT SF or a in pB ) assume A7: a in COMPLEMENT SF ; ::_thesis: a in pB then reconsider a = a as Subset of (DiscrWithInfin (X,x0)) ; a ` in SF by A7, SETFAM_1:def_7; then a ` in { {b} where b is Element of F : verum } by EQREL_1:37; then consider b being Element of F such that A8: a ` = {b} ; reconsider b = b as Element of X by Def5; {b} ` in AX ; hence a in pB by A2, A8, XBOOLE_0:def_3; ::_thesis: verum end; F = union SF by EQREL_1:def_4; then A9: a = meet (COMPLEMENT SF) by A4, TOPS_2:6; COMPLEMENT SF is finite by A5, TOPS_2:8; then Intersect (COMPLEMENT SF) in FinMeetCl pB by A6, CANTOR_1:def_3; hence a in FinMeetCl pB by A9, SETFAM_1:def_9; ::_thesis: verum end; end; end; A10: pB c= FinMeetCl pB by CANTOR_1:4; A11: B0 c= FinMeetCl pB proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B0 or a in FinMeetCl pB ) assume a in B0 ; ::_thesis: a in FinMeetCl pB then ( a in SX \ {{x0}} or a in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def_3; then ( a in pB or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def_3; hence a in FinMeetCl pB by A10, A3; ::_thesis: verum end; A12: B0 c= the topology of (DiscrWithInfin (X,x0)) by TOPS_2:64; AX c= { (F `) where F is Subset of X : F is finite } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AX or a in { (F `) where F is Subset of X : F is finite } ) assume a in AX ; ::_thesis: a in { (F `) where F is Subset of X : F is finite } then ex x being Element of X st a = {x} ` ; hence a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: verum end; then pB c= B0 by A1, XBOOLE_1:9; then pB c= the topology of (DiscrWithInfin (X,x0)) by A12, XBOOLE_1:1; then FinMeetCl pB c= FinMeetCl the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:14; then FinMeetCl pB c= the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:5; then FinMeetCl pB is Basis of (DiscrWithInfin (X,x0)) by A11, WAYBEL19:22; then pB is prebasis of (DiscrWithInfin (X,x0)) by YELLOW_9:23; hence ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } ; ::_thesis: verum end; begin theorem :: TOPGEN_2:36 for T being TopSpace for F being Subset-Family of T for I being non empty Subset-Family of F st ( for G being set st G in I holds F \ G is finite ) holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T for I being non empty Subset-Family of F st ( for G being set st G in I holds F \ G is finite ) holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) let F be Subset-Family of T; ::_thesis: for I being non empty Subset-Family of F st ( for G being set st G in I holds F \ G is finite ) holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) let I be non empty Subset-Family of F; ::_thesis: ( ( for G being set st G in I holds F \ G is finite ) implies Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ) set G0 = the Element of I; reconsider G0 = the Element of I as Subset-Family of T by XBOOLE_1:1; set Z = { (Cl (union G)) where G is Subset-Family of T : G in I } ; A1: Cl (union G0) in { (Cl (union G)) where G is Subset-Family of T : G in I } ; then reconsider Z9 = { (Cl (union G)) where G is Subset-Family of T : G in I } as non empty set ; assume A2: for G being set st G in I holds F \ G is finite ; ::_thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) :: according to XBOOLE_0:def_10 ::_thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) c= Cl (union F) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl (union F) or a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ) assume that A3: a in Cl (union F) and A4: not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; ::_thesis: contradiction reconsider a = a as Point of T by A3; not a in meet Z9 by A4, XBOOLE_0:def_3; then consider b being set such that A5: b in { (Cl (union G)) where G is Subset-Family of T : G in I } and A6: not a in b by SETFAM_1:def_1; consider G being Subset-Family of T such that A7: b = Cl (union G) and A8: G in I by A5; A9: not T is empty by A3; then clf (F \ G) c= clf F by PCOMPS_1:14, XBOOLE_1:36; then A10: union (clf (F \ G)) c= union (clf F) by ZFMISC_1:77; F = G \/ (F \ G) by A8, XBOOLE_1:45; then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:78; then Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) by PRE_TOPC:20; then a in Cl (union (F \ G)) by A3, A6, A7, XBOOLE_0:def_3; then a in union (clf (F \ G)) by A2, A8, A9, PCOMPS_1:16; hence contradiction by A4, A10, XBOOLE_0:def_3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) or a in Cl (union F) ) assume A11: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; ::_thesis: a in Cl (union F) percases ( a in union (clf F) or a in meet Z9 ) by A11, XBOOLE_0:def_3; suppose a in union (clf F) ; ::_thesis: a in Cl (union F) then consider b being set such that A12: a in b and A13: b in clf F by TARSKI:def_4; ex W being Subset of T st ( b = Cl W & W in F ) by A13, PCOMPS_1:def_2; then b c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74; hence a in Cl (union F) by A12; ::_thesis: verum end; supposeA14: a in meet Z9 ; ::_thesis: a in Cl (union F) union G0 c= union F by ZFMISC_1:77; then A15: Cl (union G0) c= Cl (union F) by PRE_TOPC:19; a in Cl (union G0) by A1, A14, SETFAM_1:def_1; hence a in Cl (union F) by A15; ::_thesis: verum end; end; end; theorem :: TOPGEN_2:37 for T being TopSpace for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) let F be Subset-Family of T; ::_thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) set Z = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ; F \ F = {} by XBOOLE_1:37; then A1: Cl (union F) in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ; then reconsider Z9 = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } as non empty set ; thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) :: according to XBOOLE_0:def_10 ::_thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) c= Cl (union F) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl (union F) or a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ) assume that A2: a in Cl (union F) and A3: not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ; ::_thesis: contradiction reconsider a = a as Point of T by A2; not a in meet Z9 by A3, XBOOLE_0:def_3; then consider b being set such that A4: b in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } and A5: not a in b by SETFAM_1:def_1; consider G being Subset-Family of T such that A6: b = Cl (union G) and A7: G c= F and A8: F \ G is finite by A4; A9: not T is empty by A2; then clf (F \ G) c= clf F by PCOMPS_1:14, XBOOLE_1:36; then A10: union (clf (F \ G)) c= union (clf F) by ZFMISC_1:77; F = G \/ (F \ G) by A7, XBOOLE_1:45; then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:78; then Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) by PRE_TOPC:20; then a in Cl (union (F \ G)) by A2, A5, A6, XBOOLE_0:def_3; then a in union (clf (F \ G)) by A8, A9, PCOMPS_1:16; hence contradiction by A3, A10, XBOOLE_0:def_3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) or a in Cl (union F) ) assume A11: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ; ::_thesis: a in Cl (union F) percases ( a in union (clf F) or a in meet Z9 ) by A11, XBOOLE_0:def_3; suppose a in union (clf F) ; ::_thesis: a in Cl (union F) then consider b being set such that A12: a in b and A13: b in clf F by TARSKI:def_4; ex W being Subset of T st ( b = Cl W & W in F ) by A13, PCOMPS_1:def_2; then b c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74; hence a in Cl (union F) by A12; ::_thesis: verum end; suppose a in meet Z9 ; ::_thesis: a in Cl (union F) hence a in Cl (union F) by A1, SETFAM_1:def_1; ::_thesis: verum end; end; end; theorem :: TOPGEN_2:38 for X being set for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopSpace ) holds ex B being Subset-Family of X st ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) proof let X be set ; ::_thesis: for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopSpace ) holds ex B being Subset-Family of X st ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) let O be Subset-Family of (bool X); ::_thesis: ( ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopSpace ) implies ex B being Subset-Family of X st ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) ) assume A1: for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopSpace ; ::_thesis: ex B being Subset-Family of X st ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) reconsider B = Intersect O as Subset-Family of X ; set T = TopStruct(# X,B #); take B ; ::_thesis: ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) thus B = Intersect O ; ::_thesis: ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) A2: TopStruct(# X,B #) is TopSpace-like proof now__::_thesis:_(_the_carrier_of_TopStruct(#_X,B_#)_in_bool_the_carrier_of_TopStruct(#_X,B_#)_&_(_for_a_being_set_st_a_in_O_holds_ the_carrier_of_TopStruct(#_X,B_#)_in_a_)_) thus the carrier of TopStruct(# X,B #) in bool the carrier of TopStruct(# X,B #) by ZFMISC_1:def_1; ::_thesis: for a being set st a in O holds the carrier of TopStruct(# X,B #) in a let a be set ; ::_thesis: ( a in O implies the carrier of TopStruct(# X,B #) in a ) assume A3: a in O ; ::_thesis: the carrier of TopStruct(# X,B #) in a then reconsider o = a as Subset-Family of X ; TopStruct(# X,o #) is TopSpace by A1, A3; hence the carrier of TopStruct(# X,B #) in a by PRE_TOPC:def_1; ::_thesis: verum end; hence the carrier of TopStruct(# X,B #) in the topology of TopStruct(# X,B #) by SETFAM_1:43; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K32(K32( the carrier of TopStruct(# X,B #))) holds ( not b1 c= the topology of TopStruct(# X,B #) or union b1 in the topology of TopStruct(# X,B #) ) ) & ( for b1, b2 being Element of K32( the carrier of TopStruct(# X,B #)) holds ( not b1 in the topology of TopStruct(# X,B #) or not b2 in the topology of TopStruct(# X,B #) or b1 /\ b2 in the topology of TopStruct(# X,B #) ) ) ) hereby ::_thesis: for b1, b2 being Element of K32( the carrier of TopStruct(# X,B #)) holds ( not b1 in the topology of TopStruct(# X,B #) or not b2 in the topology of TopStruct(# X,B #) or b1 /\ b2 in the topology of TopStruct(# X,B #) ) let a be Subset-Family of TopStruct(# X,B #); ::_thesis: ( a c= the topology of TopStruct(# X,B #) implies union a in the topology of TopStruct(# X,B #) ) assume A4: a c= the topology of TopStruct(# X,B #) ; ::_thesis: union a in the topology of TopStruct(# X,B #) now__::_thesis:_for_b_being_set_st_b_in_O_holds_ union_a_in_b let b be set ; ::_thesis: ( b in O implies union a in b ) assume A5: b in O ; ::_thesis: union a in b then reconsider o = b as Subset-Family of X ; B c= b by A5, MSSUBFAM:2; then A6: a c= o by A4, XBOOLE_1:1; TopStruct(# X,o #) is TopSpace by A1, A5; hence union a in b by A6, PRE_TOPC:def_1; ::_thesis: verum end; hence union a in the topology of TopStruct(# X,B #) by SETFAM_1:43; ::_thesis: verum end; let a, b be Subset of TopStruct(# X,B #); ::_thesis: ( not a in the topology of TopStruct(# X,B #) or not b in the topology of TopStruct(# X,B #) or a /\ b in the topology of TopStruct(# X,B #) ) assume that A7: a in the topology of TopStruct(# X,B #) and A8: b in the topology of TopStruct(# X,B #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,B #) now__::_thesis:_for_c_being_set_st_c_in_O_holds_ a_/\_b_in_c let c be set ; ::_thesis: ( c in O implies a /\ b in c ) assume A9: c in O ; ::_thesis: a /\ b in c then reconsider o = c as Subset-Family of X ; A10: b in o by A8, A9, SETFAM_1:43; A11: TopStruct(# X,o #) is TopSpace by A1, A9; a in o by A7, A9, SETFAM_1:43; hence a /\ b in c by A10, A11, PRE_TOPC:def_1; ::_thesis: verum end; hence a /\ b in the topology of TopStruct(# X,B #) by SETFAM_1:43; ::_thesis: verum end; hence TopStruct(# X,B #) is TopSpace ; ::_thesis: ( ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T ) ) thus for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ::_thesis: for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T ) holds TopStruct(# X,B #) is TopExtension of T proof let o be Subset-Family of X; ::_thesis: ( o in O implies TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) assume A12: o in O ; ::_thesis: TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) reconsider S = TopStruct(# X,o #) as TopSpace by A1, A12; Intersect O c= o by A12, MSSUBFAM:2; then S is TopExtension of TopStruct(# X,B #) by YELLOW_9:def_5; hence TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ; ::_thesis: verum end; reconsider TT = TopStruct(# X,B #) as TopSpace by A2; let T9 be TopSpace; ::_thesis: ( the carrier of T9 = X & ( for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T9 ) implies TopStruct(# X,B #) is TopExtension of T9 ) assume that A13: the carrier of T9 = X and A14: for o being Subset-Family of X st o in O holds TopStruct(# X,o #) is TopExtension of T9 ; ::_thesis: TopStruct(# X,B #) is TopExtension of T9 now__::_thesis:_for_a_being_set_st_a_in_O_holds_ the_topology_of_T9_c=_a let a be set ; ::_thesis: ( a in O implies the topology of T9 c= a ) assume A15: a in O ; ::_thesis: the topology of T9 c= a then reconsider o = a as Subset-Family of X ; TopStruct(# X,o #) is TopExtension of T9 by A14, A15; hence the topology of T9 c= a by YELLOW_9:def_5; ::_thesis: verum end; then the topology of T9 c= Intersect O by A13, MSSUBFAM:4; then TT is TopExtension of T9 by A13, YELLOW_9:def_5; hence TopStruct(# X,B #) is TopExtension of T9 ; ::_thesis: verum end; theorem :: TOPGEN_2:39 for X being set for O being Subset-Family of (bool X) ex B being Subset-Family of X st ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) proof reconsider e = {} (bool {}), tE = {({} {})} as Subset-Family of {} ; reconsider E = {} (bool (bool {})) as empty Subset-Family of (bool {}) ; let X be set ; ::_thesis: for O being Subset-Family of (bool X) ex B being Subset-Family of X st ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) let O be Subset-Family of (bool X); ::_thesis: ex B being Subset-Family of X st ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) reconsider B = UniCl (FinMeetCl (union O)) as Subset-Family of X ; take B ; ::_thesis: ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) thus B = UniCl (FinMeetCl (union O)) ; ::_thesis: ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) reconsider dT = TopStruct(# {},tE #) as discrete TopStruct by TDLAT_3:def_1, ZFMISC_1:1; A1: UniCl tE = {{},{}} by YELLOW_9:11; A2: {{},{}} = tE by ENUMSET1:29; A3: FinMeetCl tE = {{},{}} by YELLOW_9:11; A4: now__::_thesis:_(_X_is_empty_implies_(_(_union_O_=_e_or_union_O_=_tE_)_&_FinMeetCl_(union_E)_=_the_topology_of_dT_&_TopStruct(#_X,B_#)_is_TopSpace_)_) assume A5: X is empty ; ::_thesis: ( ( union O = e or union O = tE ) & FinMeetCl (union E) = the topology of dT & TopStruct(# X,B #) is TopSpace ) hence A6: ( union O = e or union O = tE ) by ZFMISC_1:1, ZFMISC_1:33; ::_thesis: ( FinMeetCl (union E) = the topology of dT & TopStruct(# X,B #) is TopSpace ) thus FinMeetCl (union E) = the topology of dT by YELLOW_9:17; ::_thesis: TopStruct(# X,B #) is TopSpace hence TopStruct(# X,B #) is TopSpace by A3, A2, A5, A6, YELLOW_9:11; ::_thesis: verum end; hence TopStruct(# X,B #) is TopSpace by CANTOR_1:15; ::_thesis: ( ( for o being Subset-Family of X st o in O holds TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) ) ) reconsider TT = TopStruct(# X,B #) as TopSpace by A4, CANTOR_1:15; hereby ::_thesis: for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) holds T is TopExtension of TopStruct(# X,B #) let o be Subset-Family of X; ::_thesis: ( o in O implies TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) set S = TopStruct(# X,o #); A7: FinMeetCl (union O) c= B by CANTOR_1:1; assume o in O ; ::_thesis: TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) then A8: o c= union O by ZFMISC_1:74; union O c= FinMeetCl (union O) by CANTOR_1:4; then o c= FinMeetCl (union O) by A8, XBOOLE_1:1; then the topology of TopStruct(# X,o #) c= the topology of TT by A7, XBOOLE_1:1; hence TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) by YELLOW_9:def_5; ::_thesis: verum end; let T be TopSpace; ::_thesis: ( the carrier of T = X & ( for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ) implies T is TopExtension of TopStruct(# X,B #) ) assume that A9: the carrier of T = X and A10: for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(# X,o #) ; ::_thesis: T is TopExtension of TopStruct(# X,B #) thus the carrier of T = the carrier of TopStruct(# X,B #) by A9; :: according to YELLOW_9:def_5 ::_thesis: the topology of TopStruct(# X,B #) c= the topology of T A11: ( X <> {} implies not T is empty ) by A9; now__::_thesis:_for_a_being_set_st_a_in_O_holds_ a_c=_the_topology_of_T let a be set ; ::_thesis: ( a in O implies a c= the topology of T ) assume A12: a in O ; ::_thesis: a c= the topology of T then reconsider o = a as Subset-Family of X ; T is TopExtension of TopStruct(# X,o #) by A10, A12; hence a c= the topology of T by YELLOW_9:def_5; ::_thesis: verum end; then union O c= the topology of T by ZFMISC_1:76; then FinMeetCl (union O) c= FinMeetCl the topology of T by A9, CANTOR_1:14; then A13: B c= UniCl (FinMeetCl the topology of T) by A9, CANTOR_1:9; X in the topology of T by A9, PRE_TOPC:def_1; hence the topology of TopStruct(# X,B #) c= the topology of T by A1, A3, A2, A4, A13, A11, CANTOR_1:7, ZFMISC_1:31; ::_thesis: verum end;