:: YELLOW_8 semantic presentation begin theorem Th1: :: YELLOW_8:1 for X, A, B being set st A in Fin X & B c= A holds B in Fin X proof let X, A, B be set ; ::_thesis: ( A in Fin X & B c= A implies B in Fin X ) assume that A1: A in Fin X and A2: B c= A ; ::_thesis: B in Fin X A c= X by A1, FINSUB_1:def_5; then B c= X by A2, XBOOLE_1:1; hence B in Fin X by A1, A2, FINSUB_1:def_5; ::_thesis: verum end; theorem Th2: :: YELLOW_8:2 for X being set for F being Subset-Family of X st F c= Fin X holds meet F in Fin X proof let X be set ; ::_thesis: for F being Subset-Family of X st F c= Fin X holds meet F in Fin X let F be Subset-Family of X; ::_thesis: ( F c= Fin X implies meet F in Fin X ) assume A1: F c= Fin X ; ::_thesis: meet F in Fin X percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet F in Fin X hence meet F in Fin X by FINSUB_1:7, SETFAM_1:1; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet F in Fin X then consider A being set such that A2: A in F by XBOOLE_0:def_1; meet F c= A by A2, SETFAM_1:3; hence meet F in Fin X by A1, A2, Th1; ::_thesis: verum end; end; end; begin theorem Th3: :: YELLOW_8:3 for X being set for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent proof let X be set ; ::_thesis: for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent let F be Subset-Family of X; ::_thesis: F, COMPLEMENT F are_equipotent deffunc H1( set ) -> Element of bool X = X \ \$1; consider f being Function such that A1: dom f = F and A2: for x being set st x in F holds f . x = H1(x) from FUNCT_1:sch_3(); take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F ) thus f is one-to-one ::_thesis: ( dom f = F & rng f = COMPLEMENT F ) proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A3: x1 in dom f and A4: x2 in dom f and A5: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4; X1 ` = f . x1 by A1, A2, A3 .= X2 ` by A1, A2, A4, A5 ; hence x1 = (X2 `) ` .= x2 ; ::_thesis: verum end; thus dom f = F by A1; ::_thesis: rng f = COMPLEMENT F thus rng f c= COMPLEMENT F :: according to XBOOLE_0:def_10 ::_thesis: COMPLEMENT F c= rng f proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng f or e in COMPLEMENT F ) assume e in rng f ; ::_thesis: e in COMPLEMENT F then consider u being set such that A6: u in dom f and A7: e = f . u by FUNCT_1:def_3; reconsider Y = u as Subset of X by A1, A6; e = Y ` by A1, A2, A6, A7; hence e in COMPLEMENT F by A1, A6, SETFAM_1:35; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in COMPLEMENT F or e in rng f ) assume A8: e in COMPLEMENT F ; ::_thesis: e in rng f then reconsider Y = e as Subset of X ; A9: Y ` in F by A8, SETFAM_1:def_7; e = (Y `) ` .= f . (Y `) by A2, A9 ; hence e in rng f by A1, A9, FUNCT_1:def_3; ::_thesis: verum end; theorem Th4: :: YELLOW_8:4 for X, Y being set st X,Y are_equipotent & X is countable holds Y is countable proof let X, Y be set ; ::_thesis: ( X,Y are_equipotent & X is countable implies Y is countable ) assume ( X,Y are_equipotent & card X c= omega ) ; :: according to CARD_3:def_14 ::_thesis: Y is countable hence card Y c= omega by CARD_1:5; :: according to CARD_3:def_14 ::_thesis: verum end; theorem :: YELLOW_8:5 for X being 1-sorted for F being Subset-Family of X for P being Subset of X holds ( P ` in COMPLEMENT F iff P in F ) proof let X be 1-sorted ; ::_thesis: for F being Subset-Family of X for P being Subset of X holds ( P ` in COMPLEMENT F iff P in F ) let F be Subset-Family of X; ::_thesis: for P being Subset of X holds ( P ` in COMPLEMENT F iff P in F ) let P be Subset of X; ::_thesis: ( P ` in COMPLEMENT F iff P in F ) P = (P `) ` ; hence ( P ` in COMPLEMENT F iff P in F ) by SETFAM_1:def_7; ::_thesis: verum end; theorem Th6: :: YELLOW_8:6 for X being 1-sorted for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) ` proof let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) ` let F be Subset-Family of X; ::_thesis: Intersect (COMPLEMENT F) = (union F) ` percases ( F <> {} or F = {} ) ; supposeA1: F <> {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) ` then COMPLEMENT F <> {} by SETFAM_1:32; hence Intersect (COMPLEMENT F) = meet (COMPLEMENT F) by SETFAM_1:def_9 .= ([#] the carrier of X) \ (union F) by A1, SETFAM_1:33 .= (union F) ` ; ::_thesis: verum end; suppose F = {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) ` then reconsider G = F as empty Subset-Family of X ; COMPLEMENT G = {} ; hence Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def_9, ZFMISC_1:2; ::_thesis: verum end; end; end; theorem Th7: :: YELLOW_8:7 for X being 1-sorted for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) ` proof let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) ` let F be Subset-Family of X; ::_thesis: union (COMPLEMENT F) = (Intersect F) ` thus union (COMPLEMENT F) = ((union (COMPLEMENT F)) `) ` .= (Intersect (COMPLEMENT (COMPLEMENT F))) ` by Th6 .= (Intersect F) ` ; ::_thesis: verum end; begin theorem :: YELLOW_8:8 for T being non empty TopSpace for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds A c= C ) holds A = Cl B proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds A c= C ) holds A = Cl B let A, B be Subset of T; ::_thesis: ( B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds A c= C ) implies A = Cl B ) assume that A1: ( B c= A & A is closed ) and A2: for C being Subset of T st B c= C & C is closed holds A c= C ; ::_thesis: A = Cl B thus A c= Cl B by A2, PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl B c= A thus Cl B c= A by A1, TOPS_1:5; ::_thesis: verum end; theorem Th9: :: YELLOW_8:9 for T being TopStruct for B being Basis of T for V being Subset of T st V is open holds V = union { G where G is Subset of T : ( G in B & G c= V ) } proof let T be TopStruct ; ::_thesis: for B being Basis of T for V being Subset of T st V is open holds V = union { G where G is Subset of T : ( G in B & G c= V ) } let B be Basis of T; ::_thesis: for V being Subset of T st V is open holds V = union { G where G is Subset of T : ( G in B & G c= V ) } let V be Subset of T; ::_thesis: ( V is open implies V = union { G where G is Subset of T : ( G in B & G c= V ) } ) assume A1: V is open ; ::_thesis: V = union { G where G is Subset of T : ( G in B & G c= V ) } set X = { G where G is Subset of T : ( G in B & G c= V ) } ; A2: the topology of T c= UniCl B by CANTOR_1:def_2; for x being set holds ( x in V iff ex Y being set st ( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) ) proof let x be set ; ::_thesis: ( x in V iff ex Y being set st ( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) ) hereby ::_thesis: ( ex Y being set st ( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) implies x in V ) V in the topology of T by A1, PRE_TOPC:def_2; then consider Y being Subset-Family of T such that A3: Y c= B and A4: V = union Y by A2, CANTOR_1:def_1; assume x in V ; ::_thesis: ex W being set st ( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } ) then consider W being set such that A5: x in W and A6: W in Y by A4, TARSKI:def_4; take W = W; ::_thesis: ( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } ) thus x in W by A5; ::_thesis: W in { G where G is Subset of T : ( G in B & G c= V ) } reconsider G = W as Subset of T by A6; G c= V by A4, A6, ZFMISC_1:74; hence W in { G where G is Subset of T : ( G in B & G c= V ) } by A3, A6; ::_thesis: verum end; given Y being set such that A7: x in Y and A8: Y in { G where G is Subset of T : ( G in B & G c= V ) } ; ::_thesis: x in V ex G being Subset of T st ( Y = G & G in B & G c= V ) by A8; hence x in V by A7; ::_thesis: verum end; hence V = union { G where G is Subset of T : ( G in B & G c= V ) } by TARSKI:def_4; ::_thesis: verum end; theorem Th10: :: YELLOW_8:10 for T being TopStruct for B being Basis of T for S being Subset of T st S in B holds S is open proof let T be TopStruct ; ::_thesis: for B being Basis of T for S being Subset of T st S in B holds S is open let B be Basis of T; ::_thesis: for S being Subset of T st S in B holds S is open let S be Subset of T; ::_thesis: ( S in B implies S is open ) assume A1: S in B ; ::_thesis: S is open B c= the topology of T by TOPS_2:64; hence S is open by A1, PRE_TOPC:def_2; ::_thesis: verum end; theorem :: YELLOW_8:11 for T being non empty TopSpace for B being Basis of T for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) } proof let T be non empty TopSpace; ::_thesis: for B being Basis of T for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) } let B be Basis of T; ::_thesis: for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) } let V be Subset of T; ::_thesis: Int V = union { G where G is Subset of T : ( G in B & G c= V ) } set X = { G where G is Subset of T : ( G in B & G c= V ) } ; set Y = { G where G is Subset of T : ( G in B & G c= Int V ) } ; { G where G is Subset of T : ( G in B & G c= V ) } = { G where G is Subset of T : ( G in B & G c= Int V ) } proof thus { G where G is Subset of T : ( G in B & G c= V ) } c= { G where G is Subset of T : ( G in B & G c= Int V ) } :: according to XBOOLE_0:def_10 ::_thesis: { G where G is Subset of T : ( G in B & G c= Int V ) } c= { G where G is Subset of T : ( G in B & G c= V ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in B & G c= V ) } or e in { G where G is Subset of T : ( G in B & G c= Int V ) } ) assume e in { G where G is Subset of T : ( G in B & G c= V ) } ; ::_thesis: e in { G where G is Subset of T : ( G in B & G c= Int V ) } then consider G being Subset of T such that A1: e = G and A2: G in B and A3: G c= V ; G c= Int V by A2, A3, Th10, TOPS_1:24; hence e in { G where G is Subset of T : ( G in B & G c= Int V ) } by A1, A2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in B & G c= Int V ) } or e in { G where G is Subset of T : ( G in B & G c= V ) } ) assume e in { G where G is Subset of T : ( G in B & G c= Int V ) } ; ::_thesis: e in { G where G is Subset of T : ( G in B & G c= V ) } then consider G being Subset of T such that A4: ( e = G & G in B ) and A5: G c= Int V ; Int V c= V by TOPS_1:16; then G c= V by A5, XBOOLE_1:1; hence e in { G where G is Subset of T : ( G in B & G c= V ) } by A4; ::_thesis: verum end; hence Int V = union { G where G is Subset of T : ( G in B & G c= V ) } by Th9; ::_thesis: verum end; begin definition let T be non empty TopStruct ; let x be Point of T; let F be Subset-Family of T; attrF is x -quasi_basis means :Def1: :: YELLOW_8:def 1 ( x in Intersect F & ( for S being Subset of T st S is open & x in S holds ex V being Subset of T st ( V in F & V c= S ) ) ); end; :: deftheorem Def1 defines -quasi_basis YELLOW_8:def_1_:_ for T being non empty TopStruct for x being Point of T for F being Subset-Family of T holds ( F is x -quasi_basis iff ( x in Intersect F & ( for S being Subset of T st S is open & x in S holds ex V being Subset of T st ( V in F & V c= S ) ) ) ); registration let T be non empty TopStruct ; let x be Point of T; cluster open x -quasi_basis for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is open & b1 is x -quasi_basis ) proof defpred S1[ set ] means ( T in the topology of T & x in T ); set IT = { S where S is Subset of T : S1[S] } ; { S where S is Subset of T : S1[S] } is Subset-Family of T from DOMAIN_1:sch_7(); then reconsider IT = { S where S is Subset of T : S1[S] } as Subset-Family of T ; take IT ; ::_thesis: ( IT is open & IT is x -quasi_basis ) IT c= the topology of T proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in IT or e in the topology of T ) assume e in IT ; ::_thesis: e in the topology of T then ex S being Subset of T st ( S = e & S in the topology of T & x in S ) ; hence e in the topology of T ; ::_thesis: verum end; hence IT is open by TOPS_2:64; ::_thesis: IT is x -quasi_basis now__::_thesis:_for_e_being_set_st_e_in_IT_holds_ x_in_e let e be set ; ::_thesis: ( e in IT implies x in e ) assume e in IT ; ::_thesis: x in e then ex S being Subset of T st ( S = e & S in the topology of T & x in S ) ; hence x in e ; ::_thesis: verum end; hence x in Intersect IT by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for S being Subset of T st S is open & x in S holds ex V being Subset of T st ( V in IT & V c= S ) let S be Subset of T; ::_thesis: ( S is open & x in S implies ex V being Subset of T st ( V in IT & V c= S ) ) assume that A1: S is open and A2: x in S ; ::_thesis: ex V being Subset of T st ( V in IT & V c= S ) take V = S; ::_thesis: ( V in IT & V c= S ) V in the topology of T by A1, PRE_TOPC:def_2; hence V in IT by A2; ::_thesis: V c= S thus V c= S ; ::_thesis: verum end; end; definition let T be non empty TopStruct ; let x be Point of T; mode Basis of x is open x -quasi_basis Subset-Family of T; end; theorem Th12: :: YELLOW_8:12 for T being non empty TopStruct for x being Point of T for B being Basis of x for V being Subset of T st V in B holds ( V is open & x in V ) proof let T be non empty TopStruct ; ::_thesis: for x being Point of T for B being Basis of x for V being Subset of T st V in B holds ( V is open & x in V ) let x be Point of T; ::_thesis: for B being Basis of x for V being Subset of T st V in B holds ( V is open & x in V ) let B be Basis of x; ::_thesis: for V being Subset of T st V in B holds ( V is open & x in V ) let V be Subset of T; ::_thesis: ( V in B implies ( V is open & x in V ) ) assume A1: V in B ; ::_thesis: ( V is open & x in V ) B c= the topology of T by TOPS_2:64; hence V is open by A1, PRE_TOPC:def_2; ::_thesis: x in V x in Intersect B by Def1; hence x in V by A1, SETFAM_1:43; ::_thesis: verum end; theorem :: YELLOW_8:13 for T being non empty TopStruct for x being Point of T for B being Basis of x for V being Subset of T st x in V & V is open holds ex W being Subset of T st ( W in B & W c= V ) by Def1; theorem :: YELLOW_8:14 for T being non empty TopStruct for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds P is Basis of T proof let T be non empty TopStruct ; ::_thesis: for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds P is Basis of T let P be Subset-Family of T; ::_thesis: ( P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) implies P is Basis of T ) assume that A1: P c= the topology of T and A2: for x being Point of T ex B being Basis of x st B c= P ; ::_thesis: P is Basis of T P is quasi_basis proof let e be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not e in the topology of T or e in UniCl P ) assume A3: e in the topology of T ; ::_thesis: e in UniCl P then reconsider S = e as Subset of T ; set X = { V where V is Subset of T : ( V in P & V c= S ) } ; A4: { V where V is Subset of T : ( V in P & V c= S ) } c= P proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { V where V is Subset of T : ( V in P & V c= S ) } or e in P ) assume e in { V where V is Subset of T : ( V in P & V c= S ) } ; ::_thesis: e in P then ex V being Subset of T st ( e = V & V in P & V c= S ) ; hence e in P ; ::_thesis: verum end; then reconsider X = { V where V is Subset of T : ( V in P & V c= S ) } as Subset-Family of T by XBOOLE_1:1; for u being set holds ( u in S iff ex Z being set st ( u in Z & Z in X ) ) proof let u be set ; ::_thesis: ( u in S iff ex Z being set st ( u in Z & Z in X ) ) hereby ::_thesis: ( ex Z being set st ( u in Z & Z in X ) implies u in S ) assume A5: u in S ; ::_thesis: ex Z being set st ( u in Z & Z in X ) then reconsider p = u as Point of T ; consider B being Basis of p such that A6: B c= P by A2; S is open by A3, PRE_TOPC:def_2; then consider W being Subset of T such that A7: W in B and A8: W c= S by A5, Def1; reconsider Z = W as set ; take Z = Z; ::_thesis: ( u in Z & Z in X ) thus u in Z by A7, Th12; ::_thesis: Z in X thus Z in X by A6, A7, A8; ::_thesis: verum end; given Z being set such that A9: u in Z and A10: Z in X ; ::_thesis: u in S ex V being Subset of T st ( V = Z & V in P & V c= S ) by A10; hence u in S by A9; ::_thesis: verum end; then S = union X by TARSKI:def_4; hence e in UniCl P by A4, CANTOR_1:def_1; ::_thesis: verum end; hence P is Basis of T by A1, TOPS_2:64; ::_thesis: verum end; definition let T be non empty TopSpace; attrT is Baire means :Def2: :: YELLOW_8:def 2 for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is everywhere_dense ) holds ex I being Subset of T st ( I = Intersect F & I is dense ); end; :: deftheorem Def2 defines Baire YELLOW_8:def_2_:_ for T being non empty TopSpace holds ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is everywhere_dense ) holds ex I being Subset of T st ( I = Intersect F & I is dense ) ); theorem :: YELLOW_8:15 for T being non empty TopSpace holds ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) holds union F is boundary ) proof let T be non empty TopSpace; ::_thesis: ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) holds union F is boundary ) hereby ::_thesis: ( ( for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) holds union F is boundary ) implies T is Baire ) assume A1: T is Baire ; ::_thesis: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) holds union F is boundary let F be Subset-Family of T; ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) implies union F is boundary ) assume that A2: F is countable and A3: for S being Subset of T st S in F holds S is nowhere_dense ; ::_thesis: union F is boundary reconsider G = COMPLEMENT F as Subset-Family of T ; A4: for S being Subset of T st S in G holds S is everywhere_dense proof let S be Subset of T; ::_thesis: ( S in G implies S is everywhere_dense ) assume S in G ; ::_thesis: S is everywhere_dense then S ` in F by SETFAM_1:def_7; then S ` is nowhere_dense by A3; hence S is everywhere_dense by TOPS_3:39; ::_thesis: verum end; G is countable by A2, Th3, Th4; then ex I being Subset of T st ( I = Intersect G & I is dense ) by A1, A4, Def2; then (union F) ` is dense by Th6; hence union F is boundary by TOPS_1:def_4; ::_thesis: verum end; assume A5: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds S is nowhere_dense ) holds union F is boundary ; ::_thesis: T is Baire let F be Subset-Family of T; :: according to YELLOW_8:def_2 ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds S is everywhere_dense ) implies ex I being Subset of T st ( I = Intersect F & I is dense ) ) assume that A6: F is countable and A7: for S being Subset of T st S in F holds S is everywhere_dense ; ::_thesis: ex I being Subset of T st ( I = Intersect F & I is dense ) reconsider I = Intersect F as Subset of T ; take I ; ::_thesis: ( I = Intersect F & I is dense ) thus I = Intersect F ; ::_thesis: I is dense reconsider G = COMPLEMENT F as Subset-Family of T ; A8: for S being Subset of T st S in G holds S is nowhere_dense proof let S be Subset of T; ::_thesis: ( S in G implies S is nowhere_dense ) assume S in G ; ::_thesis: S is nowhere_dense then S ` in F by SETFAM_1:def_7; then S ` is everywhere_dense by A7; hence S is nowhere_dense by TOPS_3:40; ::_thesis: verum end; G is countable by A6, Th3, Th4; then union G is boundary by A5, A8; then (Intersect F) ` is boundary by Th7; hence I is dense by TOPS_3:18; ::_thesis: verum end; begin definition let T be TopStruct ; let S be Subset of T; attrS is irreducible means :Def3: :: YELLOW_8:def 3 ( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds S2 = S ) ); end; :: deftheorem Def3 defines irreducible YELLOW_8:def_3_:_ for T being TopStruct for S being Subset of T holds ( S is irreducible iff ( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds S2 = S ) ) ); registration let T be TopStruct ; cluster irreducible -> non empty for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is irreducible holds not b1 is empty by Def3; end; definition let T be non empty TopSpace; let S be Subset of T; let p be Point of T; predp is_dense_point_of S means :Def4: :: YELLOW_8:def 4 ( p in S & S c= Cl {p} ); end; :: deftheorem Def4 defines is_dense_point_of YELLOW_8:def_4_:_ for T being non empty TopSpace for S being Subset of T for p being Point of T holds ( p is_dense_point_of S iff ( p in S & S c= Cl {p} ) ); theorem :: YELLOW_8:16 for T being non empty TopSpace for S being Subset of T st S is closed holds for p being Point of T st p is_dense_point_of S holds S = Cl {p} proof let T be non empty TopSpace; ::_thesis: for S being Subset of T st S is closed holds for p being Point of T st p is_dense_point_of S holds S = Cl {p} let S be Subset of T; ::_thesis: ( S is closed implies for p being Point of T st p is_dense_point_of S holds S = Cl {p} ) assume A1: S is closed ; ::_thesis: for p being Point of T st p is_dense_point_of S holds S = Cl {p} let p be Point of T; ::_thesis: ( p is_dense_point_of S implies S = Cl {p} ) assume that A2: p in S and A3: S c= Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: S = Cl {p} {p} c= S by A2, ZFMISC_1:31; then Cl {p} c= S by A1, TOPS_1:5; hence S = Cl {p} by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th17: :: YELLOW_8:17 for T being non empty TopSpace for p being Point of T holds Cl {p} is irreducible proof let T be non empty TopSpace; ::_thesis: for p being Point of T holds Cl {p} is irreducible let p be Point of T; ::_thesis: Cl {p} is irreducible assume A1: not Cl {p} is irreducible ; ::_thesis: contradiction not Cl {p} is empty by PCOMPS_1:2; then consider S1, S2 being Subset of T such that A2: ( S1 is closed & S2 is closed ) and A3: Cl {p} = S1 \/ S2 and A4: ( S1 <> Cl {p} & S2 <> Cl {p} ) by A1, Def3; ( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1; then ( p in S1 or p in S2 ) by A3, XBOOLE_0:def_3; then ( {p} c= S1 or {p} c= S2 ) by ZFMISC_1:31; then A5: ( Cl {p} c= S1 or Cl {p} c= S2 ) by A2, TOPS_1:5; ( S1 c= Cl {p} & S2 c= Cl {p} ) by A3, XBOOLE_1:7; hence contradiction by A4, A5, XBOOLE_0:def_10; ::_thesis: verum end; registration let T be non empty TopSpace; cluster irreducible for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is irreducible proof set p = the Point of T; Cl { the Point of T} is irreducible by Th17; hence ex b1 being Subset of T st b1 is irreducible ; ::_thesis: verum end; end; definition let T be non empty TopSpace; attrT is sober means :Def5: :: YELLOW_8:def 5 for S being irreducible Subset of T ex p being Point of T st ( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds p = q ) ); end; :: deftheorem Def5 defines sober YELLOW_8:def_5_:_ for T being non empty TopSpace holds ( T is sober iff for S being irreducible Subset of T ex p being Point of T st ( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds p = q ) ) ); theorem Th18: :: YELLOW_8:18 for T being non empty TopSpace for p being Point of T holds p is_dense_point_of Cl {p} proof let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of Cl {p} let p be Point of T; ::_thesis: p is_dense_point_of Cl {p} ( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1; hence p in Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: Cl {p} c= Cl {p} thus Cl {p} c= Cl {p} ; ::_thesis: verum end; theorem Th19: :: YELLOW_8:19 for T being non empty TopSpace for p being Point of T holds p is_dense_point_of {p} proof let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of {p} let p be Point of T; ::_thesis: p is_dense_point_of {p} thus p in {p} by TARSKI:def_1; :: according to YELLOW_8:def_4 ::_thesis: {p} c= Cl {p} thus {p} c= Cl {p} by PRE_TOPC:18; ::_thesis: verum end; theorem Th20: :: YELLOW_8:20 for T being non empty TopSpace for G, F being Subset of T st G is open & F is closed holds F \ G is closed proof let T be non empty TopSpace; ::_thesis: for G, F being Subset of T st G is open & F is closed holds F \ G is closed let G, F be Subset of T; ::_thesis: ( G is open & F is closed implies F \ G is closed ) assume A1: ( G is open & F is closed ) ; ::_thesis: F \ G is closed F \ G = F /\ (G `) by SUBSET_1:13; hence F \ G is closed by A1; ::_thesis: verum end; theorem Th21: :: YELLOW_8:21 for T being non empty Hausdorff TopSpace for S being irreducible Subset of T holds S is trivial proof let T be non empty Hausdorff TopSpace; ::_thesis: for S being irreducible Subset of T holds S is trivial let S be irreducible Subset of T; ::_thesis: S is trivial assume not S is trivial ; ::_thesis: contradiction then consider x, y being Point of T such that A1: ( x in S & y in S ) and A2: x <> y by SUBSET_1:45; consider W, V being Subset of T such that A3: ( W is open & V is open ) and A4: ( x in W & y in V ) and A5: W misses V by A2, PRE_TOPC:def_10; set S1 = S \ W; set S2 = S \ V; A6: ( S \ W <> S & S \ V <> S ) by A4, A1, XBOOLE_0:def_5; S is closed by Def3; then A7: ( S \ W is closed & S \ V is closed ) by A3, Th20; A8: W /\ V = {} by A5, XBOOLE_0:def_7; (S \ W) \/ (S \ V) = S \ (W /\ V) by XBOOLE_1:54 .= S by A8 ; hence contradiction by A7, A6, Def3; ::_thesis: verum end; registration let T be non empty Hausdorff TopSpace; cluster irreducible -> trivial for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is irreducible holds b1 is trivial by Th21; end; theorem Th22: :: YELLOW_8:22 for T being non empty Hausdorff TopSpace holds T is sober proof let T be non empty Hausdorff TopSpace; ::_thesis: T is sober let S be irreducible Subset of T; :: according to YELLOW_8:def_5 ::_thesis: ex p being Point of T st ( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds p = q ) ) consider d being Element of S such that A1: S = {d} by SUBSET_1:46; reconsider d = d as Point of T ; take d ; ::_thesis: ( d is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds d = q ) ) thus d is_dense_point_of S by A1, Th19; ::_thesis: for q being Point of T st q is_dense_point_of S holds d = q let p be Point of T; ::_thesis: ( p is_dense_point_of S implies d = p ) assume p is_dense_point_of S ; ::_thesis: d = p then p in S by Def4; hence d = p by A1, TARSKI:def_1; ::_thesis: verum end; registration cluster non empty TopSpace-like Hausdorff -> non empty sober for TopStruct ; coherence for b1 being non empty TopSpace st b1 is Hausdorff holds b1 is sober by Th22; end; registration cluster non empty TopSpace-like sober for TopStruct ; existence ex b1 being non empty TopSpace st b1 is sober proof set T = the non empty Hausdorff TopSpace; take the non empty Hausdorff TopSpace ; ::_thesis: the non empty Hausdorff TopSpace is sober thus the non empty Hausdorff TopSpace is sober ; ::_thesis: verum end; end; theorem Th23: :: YELLOW_8:23 for T being non empty TopSpace holds ( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds p = q ) proof let T be non empty TopSpace; ::_thesis: ( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds p = q ) thus ( T is T_0 implies for p, q being Point of T st Cl {p} = Cl {q} holds p = q ) by TSP_1:def_5; ::_thesis: ( ( for p, q being Point of T st Cl {p} = Cl {q} holds p = q ) implies T is T_0 ) assume for p, q being Point of T st Cl {p} = Cl {q} holds p = q ; ::_thesis: T is T_0 then for p, q being Point of T st p <> q holds Cl {p} <> Cl {q} ; hence T is T_0 by TSP_1:def_5; ::_thesis: verum end; theorem Th24: :: YELLOW_8:24 for T being non empty sober TopSpace holds T is T_0 proof let T be non empty sober TopSpace; ::_thesis: T is T_0 for p, q being Point of T st Cl {p} = Cl {q} holds p = q proof let p, q be Point of T; ::_thesis: ( Cl {p} = Cl {q} implies p = q ) assume A1: Cl {p} = Cl {q} ; ::_thesis: p = q Cl {p} is irreducible by Th17; then consider r being Point of T such that r is_dense_point_of Cl {p} and A2: for q being Point of T st q is_dense_point_of Cl {p} holds r = q by Def5; p = r by A2, Th18; hence p = q by A1, A2, Th18; ::_thesis: verum end; hence T is T_0 by Th23; ::_thesis: verum end; registration cluster non empty TopSpace-like sober -> non empty T_0 for TopStruct ; coherence for b1 being non empty TopSpace st b1 is sober holds b1 is T_0 by Th24; end; definition let X be set ; func CofinTop X -> strict TopStruct means :Def6: :: YELLOW_8:def 6 ( the carrier of it = X & COMPLEMENT the topology of it = {X} \/ (Fin X) ); existence ex b1 being strict TopStruct st ( the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) ) proof ( {X} c= bool X & Fin X c= bool X ) by FINSUB_1:13, ZFMISC_1:68; then reconsider F = {X} \/ (Fin X) as Subset-Family of X by XBOOLE_1:8; reconsider F = F as Subset-Family of X ; take T = TopStruct(# X,(COMPLEMENT F) #); ::_thesis: ( the carrier of T = X & COMPLEMENT the topology of T = {X} \/ (Fin X) ) thus the carrier of T = X ; ::_thesis: COMPLEMENT the topology of T = {X} \/ (Fin X) thus COMPLEMENT the topology of T = {X} \/ (Fin X) ; ::_thesis: verum end; uniqueness for b1, b2 being strict TopStruct st the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) & the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) holds b1 = b2 by SETFAM_1:38; end; :: deftheorem Def6 defines CofinTop YELLOW_8:def_6_:_ for X being set for b2 being strict TopStruct holds ( b2 = CofinTop X iff ( the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) ) ); registration let X be non empty set ; cluster CofinTop X -> non empty strict ; coherence not CofinTop X is empty by Def6; end; registration let X be set ; cluster CofinTop X -> strict TopSpace-like ; coherence CofinTop X is TopSpace-like proof reconsider F = Fin X as Subset-Family of X by FINSUB_1:13; reconsider XX = {X} as Subset-Family of X by ZFMISC_1:68; set IT = CofinTop X; reconsider XX = XX as Subset-Family of X ; reconsider F = F as Subset-Family of X ; A1: the carrier of (CofinTop X) = X by Def6; A2: COMPLEMENT the topology of (CofinTop X) = {X} \/ (Fin X) by Def6; A3: the topology of (CofinTop X) = COMPLEMENT (COMPLEMENT the topology of (CofinTop X)) .= (COMPLEMENT XX) \/ (COMPLEMENT F) by A1, A2, SETFAM_1:39 .= {{}} \/ (COMPLEMENT F) by SETFAM_1:40 ; {}. X in F ; then (({} X) `) ` in F ; then [#] X in COMPLEMENT F by SETFAM_1:def_7; hence the carrier of (CofinTop X) in the topology of (CofinTop X) by A1, A3, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (CofinTop X)) holds ( not b1 c= the topology of (CofinTop X) or union b1 in the topology of (CofinTop X) ) ) & ( for b1, b2 being Element of bool the carrier of (CofinTop X) holds ( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) ) ) ) A4: {} in {{}} by TARSKI:def_1; thus for a being Subset-Family of (CofinTop X) st a c= the topology of (CofinTop X) holds union a in the topology of (CofinTop X) ::_thesis: for b1, b2 being Element of bool the carrier of (CofinTop X) holds ( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) ) proof let a be Subset-Family of (CofinTop X); ::_thesis: ( a c= the topology of (CofinTop X) implies union a in the topology of (CofinTop X) ) assume A5: a c= the topology of (CofinTop X) ; ::_thesis: union a in the topology of (CofinTop X) set b = a /\ (COMPLEMENT F); reconsider b = a /\ (COMPLEMENT F) as Subset-Family of X ; reconsider b = b as Subset-Family of X ; a /\ {{}} c= {{}} by XBOOLE_1:17; then ( a /\ {{}} = {{}} or a /\ {{}} = {} ) by ZFMISC_1:33; then A6: union (a /\ {{}}) = {} by ZFMISC_1:2, ZFMISC_1:25; A7: union a = union (a /\ the topology of (CofinTop X)) by A5, XBOOLE_1:28 .= union ((a /\ {{}}) \/ (a /\ (COMPLEMENT F))) by A3, XBOOLE_1:23 .= (union (a /\ {{}})) \/ (union (a /\ (COMPLEMENT F))) by ZFMISC_1:78 .= union b by A6 ; percases ( b = {} or b <> {} ) ; suppose b = {} ; ::_thesis: union a in the topology of (CofinTop X) hence union a in the topology of (CofinTop X) by A3, A4, A7, XBOOLE_0:def_3, ZFMISC_1:2; ::_thesis: verum end; supposeA8: b <> {} ; ::_thesis: union a in the topology of (CofinTop X) b c= COMPLEMENT F by XBOOLE_1:17; then A9: COMPLEMENT b c= Fin X by SETFAM_1:37; meet (COMPLEMENT b) = ([#] X) \ (union b) by A8, SETFAM_1:33 .= (union b) ` ; then (union b) ` in Fin X by A9, Th2; then union b in COMPLEMENT F by SETFAM_1:def_7; hence union a in the topology of (CofinTop X) by A3, A7, XBOOLE_0:def_3; ::_thesis: verum end; end; end; let a, b be Subset of (CofinTop X); ::_thesis: ( not a in the topology of (CofinTop X) or not b in the topology of (CofinTop X) or a /\ b in the topology of (CofinTop X) ) assume that A10: a in the topology of (CofinTop X) and A11: b in the topology of (CofinTop X) ; ::_thesis: a /\ b in the topology of (CofinTop X) reconsider a9 = a, b9 = b as Subset of X by Def6; percases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ; suppose ( a = {} or b = {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X) hence a /\ b in the topology of (CofinTop X) by A3, A4, XBOOLE_0:def_3; ::_thesis: verum end; supposeA12: ( a <> {} & b <> {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X) then not b in {{}} by TARSKI:def_1; then b9 in COMPLEMENT F by A3, A11, XBOOLE_0:def_3; then A13: b9 ` in Fin X by SETFAM_1:def_7; not a in {{}} by A12, TARSKI:def_1; then a9 in COMPLEMENT F by A3, A10, XBOOLE_0:def_3; then a9 ` in Fin X by SETFAM_1:def_7; then (a9 `) \/ (b9 `) in Fin X by A13, FINSUB_1:1; then (a9 /\ b9) ` in Fin X by XBOOLE_1:54; then a /\ b in COMPLEMENT F by SETFAM_1:def_7; hence a /\ b in the topology of (CofinTop X) by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; theorem Th25: :: YELLOW_8:25 for X being non empty set for P being Subset of (CofinTop X) holds ( P is closed iff ( P = X or P is finite ) ) proof let X be non empty set ; ::_thesis: for P being Subset of (CofinTop X) holds ( P is closed iff ( P = X or P is finite ) ) let P be Subset of (CofinTop X); ::_thesis: ( P is closed iff ( P = X or P is finite ) ) set T = CofinTop X; hereby ::_thesis: ( ( P = X or P is finite ) implies P is closed ) assume that A1: P is closed and A2: P <> X ; ::_thesis: P is finite P ` in the topology of (CofinTop X) by A1, PRE_TOPC:def_2; then P in COMPLEMENT the topology of (CofinTop X) by SETFAM_1:def_7; then A3: P in {X} \/ (Fin X) by Def6; not P in {X} by A2, TARSKI:def_1; then P in Fin X by A3, XBOOLE_0:def_3; hence P is finite ; ::_thesis: verum end; assume A4: ( P = X or P is finite ) ; ::_thesis: P is closed the carrier of (CofinTop X) = X by Def6; then ( P in {X} or P in Fin X ) by A4, FINSUB_1:def_5, TARSKI:def_1; then P in {X} \/ (Fin X) by XBOOLE_0:def_3; then P in COMPLEMENT the topology of (CofinTop X) by Def6; then P ` in the topology of (CofinTop X) by SETFAM_1:def_7; then P ` is open by PRE_TOPC:def_2; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem Th26: :: YELLOW_8:26 for T being non empty TopSpace st T is T_1 holds for p being Point of T holds Cl {p} = {p} proof let T be non empty TopSpace; ::_thesis: ( T is T_1 implies for p being Point of T holds Cl {p} = {p} ) assume A1: T is T_1 ; ::_thesis: for p being Point of T holds Cl {p} = {p} let p be Point of T; ::_thesis: Cl {p} = {p} {p} is closed by A1, URYSOHN1:19; then A2: Cl {p} c= {p} by TOPS_1:5; {p} c= Cl {p} by PRE_TOPC:18; hence Cl {p} = {p} by A2, XBOOLE_0:def_10; ::_thesis: verum end; registration let X be non empty set ; cluster CofinTop X -> strict T_1 ; coherence CofinTop X is T_1 proof for p being Point of (CofinTop X) holds {p} is closed by Th25; hence CofinTop X is T_1 by URYSOHN1:19; ::_thesis: verum end; end; registration let X be infinite set ; cluster CofinTop X -> strict non sober ; coherence not CofinTop X is sober proof set T = CofinTop X; reconsider S = [#] X as Subset of (CofinTop X) by Def6; S is irreducible proof X = [#] (CofinTop X) by Def6; hence ( not S is empty & S is closed ) ; :: according to YELLOW_8:def_3 ::_thesis: for S1, S2 being Subset of (CofinTop X) st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds S2 = S let S1, S2 be Subset of (CofinTop X); ::_thesis: ( S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S implies S2 = S ) assume that A1: ( S1 is closed & S2 is closed ) and A2: S = S1 \/ S2 ; ::_thesis: ( S1 = S or S2 = S ) assume ( S1 <> S & S2 <> S ) ; ::_thesis: contradiction then reconsider S19 = S1, S29 = S2 as finite set by A1, Th25; S = S19 \/ S29 by A2; hence contradiction ; ::_thesis: verum end; then reconsider S = S as irreducible Subset of (CofinTop X) ; take S ; :: according to YELLOW_8:def_5 ::_thesis: for p being Point of (CofinTop X) holds ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st ( q is_dense_point_of S & not p = q ) ) let p be Point of (CofinTop X); ::_thesis: ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st ( q is_dense_point_of S & not p = q ) ) now__::_thesis:_not_p_is_dense_point_of_S assume p is_dense_point_of S ; ::_thesis: contradiction then S c= Cl {p} by Def4; then Cl {p} is infinite ; hence contradiction by Th26; ::_thesis: verum end; hence ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st ( q is_dense_point_of S & not p = q ) ) ; ::_thesis: verum end; end; registration cluster non empty TopSpace-like T_1 non sober for TopStruct ; existence ex b1 being non empty TopSpace st ( b1 is T_1 & not b1 is sober ) proof set X = the infinite set ; take CofinTop the infinite set ; ::_thesis: ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober ) thus ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober ) ; ::_thesis: verum end; end; begin theorem Th27: :: YELLOW_8:27 for T being non empty TopSpace holds ( T is regular iff for p being Point of T for P being Subset of T st p in Int P holds ex Q being Subset of T st ( Q is closed & Q c= P & p in Int Q ) ) proof let T be non empty TopSpace; ::_thesis: ( T is regular iff for p being Point of T for P being Subset of T st p in Int P holds ex Q being Subset of T st ( Q is closed & Q c= P & p in Int Q ) ) hereby ::_thesis: ( ( for p being Point of T for P being Subset of T st p in Int P holds ex Q being Subset of T st ( Q is closed & Q c= P & p in Int Q ) ) implies T is regular ) assume A1: T is regular ; ::_thesis: for p being Point of T for P being Subset of T st p in Int P holds ex Q being Element of bool the carrier of T st ( b5 is closed & b5 c= b4 & Q in Int b5 ) let p be Point of T; ::_thesis: for P being Subset of T st p in Int P holds ex Q being Element of bool the carrier of T st ( b4 is closed & b4 c= b3 & Q in Int b4 ) let P be Subset of T; ::_thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st ( b3 is closed & b3 c= b2 & Q in Int b3 ) ) assume p in Int P ; ::_thesis: ex Q being Element of bool the carrier of T st ( b3 is closed & b3 c= b2 & Q in Int b3 ) then A2: p in ((Int P) `) ` ; percases ( P = [#] T or P <> [#] T ) ; supposeA3: P = [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st ( b3 is closed & b3 c= b2 & Q in Int b3 ) take Q = [#] T; ::_thesis: ( Q is closed & Q c= P & p in Int Q ) thus Q is closed ; ::_thesis: ( Q c= P & p in Int Q ) thus Q c= P by A3; ::_thesis: p in Int Q Int Q = Q by TOPS_1:15; hence p in Int Q ; ::_thesis: verum end; supposeA4: P <> [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st ( b3 is closed & b3 c= b2 & Q in Int b3 ) now__::_thesis:_not_(Int_P)_`_=_{} assume (Int P) ` = {} ; ::_thesis: contradiction then ((Int P) `) ` = [#] T ; then [#] T c= P by TOPS_1:16; hence contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum end; then consider W, V being Subset of T such that A5: W is open and A6: V is open and A7: p in W and A8: (Int P) ` c= V and A9: W misses V by A1, A2, COMPTS_1:def_2; A10: Int P c= P by TOPS_1:16; take Q = V ` ; ::_thesis: ( Q is closed & Q c= P & p in Int Q ) thus Q is closed by A6; ::_thesis: ( Q c= P & p in Int Q ) (Int P) ` c= Q ` by A8; then Q c= Int P by SUBSET_1:12; hence Q c= P by A10, XBOOLE_1:1; ::_thesis: p in Int Q W c= Q by A9, SUBSET_1:23; then W c= Int Q by A5, TOPS_1:24; hence p in Int Q by A7; ::_thesis: verum end; end; end; assume A11: for p being Point of T for P being Subset of T st p in Int P holds ex Q being Subset of T st ( Q is closed & Q c= P & p in Int Q ) ; ::_thesis: T is regular let p be Point of T; :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds ( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st ( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) ) let P be Subset of T; ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) ) assume that P <> {} and A12: ( P is closed & p in P ` ) ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) p in Int (P `) by A12, TOPS_1:23; then consider Q being Subset of T such that A13: Q is closed and A14: Q c= P ` and A15: p in Int Q by A11; reconsider W = Int Q as Subset of T ; take W ; ::_thesis: ex b1 being Element of bool the carrier of T st ( W is open & b1 is open & p in W & P c= b1 & W misses b1 ) take V = Q ` ; ::_thesis: ( W is open & V is open & p in W & P c= V & W misses V ) thus W is open ; ::_thesis: ( V is open & p in W & P c= V & W misses V ) thus V is open by A13; ::_thesis: ( p in W & P c= V & W misses V ) thus p in W by A15; ::_thesis: ( P c= V & W misses V ) (P `) ` c= V by A14, SUBSET_1:12; hence P c= V ; ::_thesis: W misses V Q misses V by XBOOLE_1:79; hence W misses V by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum end; theorem :: YELLOW_8:28 for T being non empty TopSpace st T is regular holds ( T is locally-compact iff for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) ) proof let T be non empty TopSpace; ::_thesis: ( T is regular implies ( T is locally-compact iff for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) ) ) assume A1: T is regular ; ::_thesis: ( T is locally-compact iff for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) ) hereby ::_thesis: ( ( for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) ) implies T is locally-compact ) assume A2: T is locally-compact ; ::_thesis: for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) let x be Point of T; ::_thesis: ex Y being Subset of T st ( x in Int Y & Y is compact ) ex Y being Subset of T st ( x in Int Y & Y c= [#] T & Y is compact ) by A2, WAYBEL_3:def_9; hence ex Y being Subset of T st ( x in Int Y & Y is compact ) ; ::_thesis: verum end; assume A3: for x being Point of T ex Y being Subset of T st ( x in Int Y & Y is compact ) ; ::_thesis: T is locally-compact let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of bool the carrier of T holds ( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of T st ( x in Int b2 & b2 c= b1 & b2 is compact ) ) let X be Subset of T; ::_thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of T st ( x in Int b1 & b1 c= X & b1 is compact ) ) assume ( x in X & X is open ) ; ::_thesis: ex b1 being Element of bool the carrier of T st ( x in Int b1 & b1 c= X & b1 is compact ) then A4: x in Int X by TOPS_1:23; consider Y being Subset of T such that A5: x in Int Y and A6: Y is compact by A3; x in (Int X) /\ (Int Y) by A5, A4, XBOOLE_0:def_4; then x in Int (X /\ Y) by TOPS_1:17; then consider Q being Subset of T such that A7: Q is closed and A8: Q c= X /\ Y and A9: x in Int Q by A1, Th27; take Q ; ::_thesis: ( x in Int Q & Q c= X & Q is compact ) thus x in Int Q by A9; ::_thesis: ( Q c= X & Q is compact ) X /\ Y c= X by XBOOLE_1:17; hence Q c= X by A8, XBOOLE_1:1; ::_thesis: Q is compact X /\ Y c= Y by XBOOLE_1:17; hence Q is compact by A6, A7, A8, COMPTS_1:9, XBOOLE_1:1; ::_thesis: verum end;