:: CONNSP_2 semantic presentation begin definition let X be non empty TopSpace; let x be Point of X; mode a_neighborhood of x -> Subset of X means :Def1: :: CONNSP_2:def 1 x in Int it; existence ex b1 being Subset of X st x in Int b1 proof take [#] X ; ::_thesis: x in Int ([#] X) Int ([#] X) = [#] X by TOPS_1:15; hence x in Int ([#] X) ; ::_thesis: verum end; end; :: deftheorem Def1 defines a_neighborhood CONNSP_2:def_1_:_ for X being non empty TopSpace for x being Point of X for b3 being Subset of X holds ( b3 is a_neighborhood of x iff x in Int b3 ); definition let X be TopSpace; let A be Subset of X; mode a_neighborhood of A -> Subset of X means :Def2: :: CONNSP_2:def 2 A c= Int it; existence ex b1 being Subset of X st A c= Int b1 proof take [#] X ; ::_thesis: A c= Int ([#] X) Int ([#] X) = [#] X by TOPS_1:15; hence A c= Int ([#] X) ; ::_thesis: verum end; end; :: deftheorem Def2 defines a_neighborhood CONNSP_2:def_2_:_ for X being TopSpace for A, b3 being Subset of X holds ( b3 is a_neighborhood of A iff A c= Int b3 ); theorem :: CONNSP_2:1 for X being non empty TopSpace for x being Point of X for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds A \/ B is a_neighborhood of x proof let X be non empty TopSpace; ::_thesis: for x being Point of X for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds A \/ B is a_neighborhood of x let x be Point of X; ::_thesis: for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds A \/ B is a_neighborhood of x let A, B be Subset of X; ::_thesis: ( A is a_neighborhood of x & B is a_neighborhood of x implies A \/ B is a_neighborhood of x ) reconsider A1 = A, B1 = B as Subset of X ; ( A1 is a_neighborhood of x & B1 is a_neighborhood of x implies A1 \/ B1 is a_neighborhood of x ) proof assume that A1: x in Int A1 and x in Int B1 ; :: according to CONNSP_2:def_1 ::_thesis: A1 \/ B1 is a_neighborhood of x A2: (Int A1) \/ (Int B1) c= Int (A1 \/ B1) by TOPS_1:20; x in (Int A1) \/ (Int B1) by A1, XBOOLE_0:def_3; hence A1 \/ B1 is a_neighborhood of x by A2, Def1; ::_thesis: verum end; hence ( A is a_neighborhood of x & B is a_neighborhood of x implies A \/ B is a_neighborhood of x ) ; ::_thesis: verum end; theorem :: CONNSP_2:2 for X being non empty TopSpace for x being Point of X for A, B being Subset of X holds ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X for A, B being Subset of X holds ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) let x be Point of X; ::_thesis: for A, B being Subset of X holds ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) let A, B be Subset of X; ::_thesis: ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) ( A is a_neighborhood of x & B is a_neighborhood of x iff ( x in Int A & x in Int B ) ) by Def1; then ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff x in (Int A) /\ (Int B) ) by XBOOLE_0:def_4; then ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff x in Int (A /\ B) ) by TOPS_1:17; hence ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) by Def1; ::_thesis: verum end; theorem Th3: :: CONNSP_2:3 for X being non empty TopSpace for U1 being Subset of X for x being Point of X st U1 is open & x in U1 holds U1 is a_neighborhood of x proof let X be non empty TopSpace; ::_thesis: for U1 being Subset of X for x being Point of X st U1 is open & x in U1 holds U1 is a_neighborhood of x let U1 be Subset of X; ::_thesis: for x being Point of X st U1 is open & x in U1 holds U1 is a_neighborhood of x let x be Point of X; ::_thesis: ( U1 is open & x in U1 implies U1 is a_neighborhood of x ) assume ( U1 is open & x in U1 ) ; ::_thesis: U1 is a_neighborhood of x then x in Int U1 by TOPS_1:23; hence U1 is a_neighborhood of x by Def1; ::_thesis: verum end; theorem Th4: :: CONNSP_2:4 for X being non empty TopSpace for U1 being Subset of X for x being Point of X st U1 is a_neighborhood of x holds x in U1 proof let X be non empty TopSpace; ::_thesis: for U1 being Subset of X for x being Point of X st U1 is a_neighborhood of x holds x in U1 let U1 be Subset of X; ::_thesis: for x being Point of X st U1 is a_neighborhood of x holds x in U1 let x be Point of X; ::_thesis: ( U1 is a_neighborhood of x implies x in U1 ) assume U1 is a_neighborhood of x ; ::_thesis: x in U1 then A1: x in Int U1 by Def1; Int U1 c= U1 by TOPS_1:16; hence x in U1 by A1; ::_thesis: verum end; theorem Th5: :: CONNSP_2:5 for X being non empty TopSpace for x being Point of X for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being non empty Subset of X st ( V is a_neighborhood of x & V is open & V c= U1 ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being non empty Subset of X st ( V is a_neighborhood of x & V is open & V c= U1 ) let x be Point of X; ::_thesis: for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being non empty Subset of X st ( V is a_neighborhood of x & V is open & V c= U1 ) let U1 be Subset of X; ::_thesis: ( U1 is a_neighborhood of x implies ex V being non empty Subset of X st ( V is a_neighborhood of x & V is open & V c= U1 ) ) assume U1 is a_neighborhood of x ; ::_thesis: ex V being non empty Subset of X st ( V is a_neighborhood of x & V is open & V c= U1 ) then x in Int U1 by Def1; then consider V being Subset of X such that A1: ( V is open & V c= U1 ) and A2: x in V by TOPS_1:22; reconsider V = V as non empty Subset of X by A2; take V ; ::_thesis: ( V is a_neighborhood of x & V is open & V c= U1 ) thus ( V is a_neighborhood of x & V is open & V c= U1 ) by A1, A2, Th3; ::_thesis: verum end; theorem Th6: :: CONNSP_2:6 for X being non empty TopSpace for x being Point of X for U1 being Subset of X holds ( U1 is a_neighborhood of x iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X for U1 being Subset of X holds ( U1 is a_neighborhood of x iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) let x be Point of X; ::_thesis: for U1 being Subset of X holds ( U1 is a_neighborhood of x iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) let U1 be Subset of X; ::_thesis: ( U1 is a_neighborhood of x iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) A1: now__::_thesis:_(_U1_is_a_neighborhood_of_x_implies_ex_V_being_non_empty_Subset_of_X_ex_V_being_Subset_of_X_st_ (_V_is_open_&_V_c=_U1_&_x_in_V_)_) assume U1 is a_neighborhood of x ; ::_thesis: ex V being non empty Subset of X ex V being Subset of X st ( V is open & V c= U1 & x in V ) then consider V being non empty Subset of X such that A2: ( V is a_neighborhood of x & V is open & V c= U1 ) by Th5; take V = V; ::_thesis: ex V being Subset of X st ( V is open & V c= U1 & x in V ) thus ex V being Subset of X st ( V is open & V c= U1 & x in V ) by A2, Th4; ::_thesis: verum end; now__::_thesis:_(_ex_V_being_Subset_of_X_st_ (_V_is_open_&_V_c=_U1_&_x_in_V_)_implies_U1_is_a_neighborhood_of_x_) given V being Subset of X such that A3: ( V is open & V c= U1 & x in V ) ; ::_thesis: U1 is a_neighborhood of x x in Int U1 by A3, TOPS_1:22; hence U1 is a_neighborhood of x by Def1; ::_thesis: verum end; hence ( U1 is a_neighborhood of x iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) by A1; ::_thesis: verum end; theorem :: CONNSP_2:7 for X being non empty TopSpace for U1 being Subset of X holds ( U1 is open iff for x being Point of X st x in U1 holds ex A being Subset of X st ( A is a_neighborhood of x & A c= U1 ) ) proof let X be non empty TopSpace; ::_thesis: for U1 being Subset of X holds ( U1 is open iff for x being Point of X st x in U1 holds ex A being Subset of X st ( A is a_neighborhood of x & A c= U1 ) ) let U1 be Subset of X; ::_thesis: ( U1 is open iff for x being Point of X st x in U1 holds ex A being Subset of X st ( A is a_neighborhood of x & A c= U1 ) ) now__::_thesis:_(_(_for_x_being_Point_of_X_st_x_in_U1_holds_ ex_A_being_Subset_of_X_st_ (_A_is_a_neighborhood_of_x_&_A_c=_U1_)_)_implies_U1_is_open_) assume A1: for x being Point of X st x in U1 holds ex A being Subset of X st ( A is a_neighborhood of x & A c= U1 ) ; ::_thesis: U1 is open for x being set holds ( x in U1 iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) proof let x be set ; ::_thesis: ( x in U1 iff ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) thus ( x in U1 implies ex V being Subset of X st ( V is open & V c= U1 & x in V ) ) ::_thesis: ( ex V being Subset of X st ( V is open & V c= U1 & x in V ) implies x in U1 ) proof assume A2: x in U1 ; ::_thesis: ex V being Subset of X st ( V is open & V c= U1 & x in V ) then reconsider x = x as Point of X ; consider S being Subset of X such that A3: S is a_neighborhood of x and A4: S c= U1 by A1, A2; consider V being Subset of X such that A5: ( V is open & V c= S & x in V ) by A3, Th6; take V ; ::_thesis: ( V is open & V c= U1 & x in V ) thus ( V is open & V c= U1 & x in V ) by A4, A5, XBOOLE_1:1; ::_thesis: verum end; given V being Subset of X such that V is open and A6: ( V c= U1 & x in V ) ; ::_thesis: x in U1 thus x in U1 by A6; ::_thesis: verum end; hence U1 is open by TOPS_1:25; ::_thesis: verum end; hence ( U1 is open iff for x being Point of X st x in U1 holds ex A being Subset of X st ( A is a_neighborhood of x & A c= U1 ) ) by Th3; ::_thesis: verum end; theorem :: CONNSP_2:8 for X being non empty TopSpace for x being Point of X for V being Subset of X holds ( V is a_neighborhood of {x} iff V is a_neighborhood of x ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X for V being Subset of X holds ( V is a_neighborhood of {x} iff V is a_neighborhood of x ) let x be Point of X; ::_thesis: for V being Subset of X holds ( V is a_neighborhood of {x} iff V is a_neighborhood of x ) let V be Subset of X; ::_thesis: ( V is a_neighborhood of {x} iff V is a_neighborhood of x ) thus ( V is a_neighborhood of {x} implies V is a_neighborhood of x ) ::_thesis: ( V is a_neighborhood of x implies V is a_neighborhood of {x} ) proof assume V is a_neighborhood of {x} ; ::_thesis: V is a_neighborhood of x then A1: {x} c= Int V by Def2; x in {x} by TARSKI:def_1; hence V is a_neighborhood of x by A1, Def1; ::_thesis: verum end; assume V is a_neighborhood of x ; ::_thesis: V is a_neighborhood of {x} then x in Int V by Def1; then for p being set st p in {x} holds p in Int V by TARSKI:def_1; then {x} c= Int V by TARSKI:def_3; hence V is a_neighborhood of {x} by Def2; ::_thesis: verum end; theorem Th9: :: CONNSP_2:9 for X being non empty TopSpace for B being non empty Subset of X for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 proof let X be non empty TopSpace; ::_thesis: for B being non empty Subset of X for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 let B be non empty Subset of X; ::_thesis: for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 let x be Point of (X | B); ::_thesis: for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 let A be Subset of (X | B); ::_thesis: for A1 being Subset of X for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 let A1 be Subset of X; ::_thesis: for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1 let x1 be Point of X; ::_thesis: ( B is open & A is a_neighborhood of x & A = A1 & x = x1 implies A1 is a_neighborhood of x1 ) assume that A1: B is open and A2: A is a_neighborhood of x and A3: ( A = A1 & x = x1 ) ; ::_thesis: A1 is a_neighborhood of x1 x in Int A by A2, Def1; then consider Q1 being Subset of (X | B) such that A4: Q1 is open and A5: ( Q1 c= A & x in Q1 ) by TOPS_1:22; Q1 in the topology of (X | B) by A4, PRE_TOPC:def_2; then consider Q being Subset of X such that A6: Q in the topology of X and A7: Q1 = Q /\ ([#] (X | B)) by PRE_TOPC:def_4; reconsider Q2 = Q as Subset of X ; Q2 is open by A6, PRE_TOPC:def_2; then A8: Q /\ B is open by A1; Q1 = Q /\ B by A7, PRE_TOPC:def_5; then x1 in Int A1 by A3, A5, A8, TOPS_1:22; hence A1 is a_neighborhood of x1 by Def1; ::_thesis: verum end; Lm1: for X being non empty TopSpace for X1 being SubSpace of X for A being Subset of X for A1 being Subset of X1 st A = A1 holds (Int A) /\ ([#] X1) c= Int A1 proof let X be non empty TopSpace; ::_thesis: for X1 being SubSpace of X for A being Subset of X for A1 being Subset of X1 st A = A1 holds (Int A) /\ ([#] X1) c= Int A1 let X1 be SubSpace of X; ::_thesis: for A being Subset of X for A1 being Subset of X1 st A = A1 holds (Int A) /\ ([#] X1) c= Int A1 let A be Subset of X; ::_thesis: for A1 being Subset of X1 st A = A1 holds (Int A) /\ ([#] X1) c= Int A1 let A1 be Subset of X1; ::_thesis: ( A = A1 implies (Int A) /\ ([#] X1) c= Int A1 ) assume A1: A = A1 ; ::_thesis: (Int A) /\ ([#] X1) c= Int A1 for p being set st p in (Int A) /\ ([#] X1) holds p in Int A1 proof let p be set ; ::_thesis: ( p in (Int A) /\ ([#] X1) implies p in Int A1 ) assume A2: p in (Int A) /\ ([#] X1) ; ::_thesis: p in Int A1 then p in Int A by XBOOLE_0:def_4; then consider Q being Subset of X such that A3: Q is open and A4: ( Q c= A & p in Q ) by TOPS_1:22; ex Q1 being Subset of X1 st ( Q1 is open & Q1 c= A1 & p in Q1 ) proof reconsider Q1 = Q /\ ([#] X1) as Subset of X1 ; take Q1 ; ::_thesis: ( Q1 is open & Q1 c= A1 & p in Q1 ) Q in the topology of X by A3, PRE_TOPC:def_2; then ( Q1 c= Q & Q1 in the topology of X1 ) by PRE_TOPC:def_4, XBOOLE_1:17; hence ( Q1 is open & Q1 c= A1 & p in Q1 ) by A1, A2, A4, PRE_TOPC:def_2, XBOOLE_0:def_4, XBOOLE_1:1; ::_thesis: verum end; hence p in Int A1 by TOPS_1:22; ::_thesis: verum end; hence (Int A) /\ ([#] X1) c= Int A1 by TARSKI:def_3; ::_thesis: verum end; theorem Th10: :: CONNSP_2:10 for X being non empty TopSpace for B being non empty Subset of X for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x proof let X be non empty TopSpace; ::_thesis: for B being non empty Subset of X for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x let B be non empty Subset of X; ::_thesis: for x being Point of (X | B) for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x let x be Point of (X | B); ::_thesis: for A being Subset of (X | B) for A1 being Subset of X for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x let A be Subset of (X | B); ::_thesis: for A1 being Subset of X for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x let A1 be Subset of X; ::_thesis: for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x let x1 be Point of X; ::_thesis: ( A1 is a_neighborhood of x1 & A = A1 & x = x1 implies A is a_neighborhood of x ) assume that A1: A1 is a_neighborhood of x1 and A2: A = A1 and A3: x = x1 ; ::_thesis: A is a_neighborhood of x x1 in Int A1 by A1, Def1; then A4: x1 in (Int A1) /\ ([#] (X | B)) by A3, XBOOLE_0:def_4; (Int A1) /\ ([#] (X | B)) c= Int A by A2, Lm1; hence A is a_neighborhood of x by A3, A4, Def1; ::_thesis: verum end; theorem Th11: :: CONNSP_2:11 for X being non empty TopSpace for A, B being Subset of X st A is a_component & A c= B holds A is_a_component_of B proof let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is a_component & A c= B holds A is_a_component_of B let A, B be Subset of X; ::_thesis: ( A is a_component & A c= B implies A is_a_component_of B ) assume that A1: A is a_component and A2: A c= B ; ::_thesis: A is_a_component_of B A3: A is connected by A1; ex A1 being Subset of (X | B) st ( A = A1 & A1 is a_component ) proof B = [#] (X | B) by PRE_TOPC:def_5; then reconsider C = A as Subset of (X | B) by A2; take A1 = C; ::_thesis: ( A = A1 & A1 is a_component ) A4: for D being Subset of (X | B) st D is connected & A1 c= D holds A1 = D proof let D be Subset of (X | B); ::_thesis: ( D is connected & A1 c= D implies A1 = D ) assume A5: D is connected ; ::_thesis: ( not A1 c= D or A1 = D ) reconsider D1 = D as Subset of X by PRE_TOPC:11; assume A6: A1 c= D ; ::_thesis: A1 = D D1 is connected by A5, CONNSP_1:23; hence A1 = D by A1, A6, CONNSP_1:def_5; ::_thesis: verum end; A1 is connected by A3, CONNSP_1:23; hence ( A = A1 & A1 is a_component ) by A4, CONNSP_1:def_5; ::_thesis: verum end; hence A is_a_component_of B by CONNSP_1:def_6; ::_thesis: verum end; theorem :: CONNSP_2:12 for X being non empty TopSpace for X1 being non empty SubSpace of X for x being Point of X for x1 being Point of X1 st x = x1 holds Component_of x1 c= Component_of x proof let X be non empty TopSpace; ::_thesis: for X1 being non empty SubSpace of X for x being Point of X for x1 being Point of X1 st x = x1 holds Component_of x1 c= Component_of x let X1 be non empty SubSpace of X; ::_thesis: for x being Point of X for x1 being Point of X1 st x = x1 holds Component_of x1 c= Component_of x let x be Point of X; ::_thesis: for x1 being Point of X1 st x = x1 holds Component_of x1 c= Component_of x let x1 be Point of X1; ::_thesis: ( x = x1 implies Component_of x1 c= Component_of x ) consider F being Subset-Family of X such that A1: for A being Subset of X holds ( A in F iff ( A is connected & x in A ) ) and A2: union F = Component_of x by CONNSP_1:def_7; reconsider Z = Component_of x1 as Subset of X by PRE_TOPC:11; A3: ( x1 in Z & Z is connected ) by CONNSP_1:23, CONNSP_1:38; assume x = x1 ; ::_thesis: Component_of x1 c= Component_of x then Z in F by A1, A3; hence Component_of x1 c= Component_of x by A2, ZFMISC_1:74; ::_thesis: verum end; definition let X be non empty TopSpace; let x be Point of X; predX is_locally_connected_in x means :Def3: :: CONNSP_2:def 3 for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being Subset of X st ( V is a_neighborhood of x & V is connected & V c= U1 ); end; :: deftheorem Def3 defines is_locally_connected_in CONNSP_2:def_3_:_ for X being non empty TopSpace for x being Point of X holds ( X is_locally_connected_in x iff for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being Subset of X st ( V is a_neighborhood of x & V is connected & V c= U1 ) ); definition let X be non empty TopSpace; attrX is locally_connected means :Def4: :: CONNSP_2:def 4 for x being Point of X holds X is_locally_connected_in x; end; :: deftheorem Def4 defines locally_connected CONNSP_2:def_4_:_ for X being non empty TopSpace holds ( X is locally_connected iff for x being Point of X holds X is_locally_connected_in x ); definition let X be non empty TopSpace; let A be Subset of X; let x be Point of X; predA is_locally_connected_in x means :Def5: :: CONNSP_2:def 5 for B being non empty Subset of X st A = B holds ex x1 being Point of (X | B) st ( x1 = x & X | B is_locally_connected_in x1 ); end; :: deftheorem Def5 defines is_locally_connected_in CONNSP_2:def_5_:_ for X being non empty TopSpace for A being Subset of X for x being Point of X holds ( A is_locally_connected_in x iff for B being non empty Subset of X st A = B holds ex x1 being Point of (X | B) st ( x1 = x & X | B is_locally_connected_in x1 ) ); definition let X be non empty TopSpace; let A be non empty Subset of X; attrA is locally_connected means :Def6: :: CONNSP_2:def 6 X | A is locally_connected ; end; :: deftheorem Def6 defines locally_connected CONNSP_2:def_6_:_ for X being non empty TopSpace for A being non empty Subset of X holds ( A is locally_connected iff X | A is locally_connected ); theorem Th13: :: CONNSP_2:13 for X being non empty TopSpace for x being Point of X holds ( X is_locally_connected_in x iff for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds ( X is_locally_connected_in x iff for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ) let x be Point of X; ::_thesis: ( X is_locally_connected_in x iff for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ) thus ( X is_locally_connected_in x implies for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ) ::_thesis: ( ( for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ) implies X is_locally_connected_in x ) proof assume A1: X is_locally_connected_in x ; ::_thesis: for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x let V, S be Subset of X; ::_thesis: ( V is a_neighborhood of x & S is_a_component_of V & x in S implies S is a_neighborhood of x ) assume that A2: V is a_neighborhood of x and A3: S is_a_component_of V and A4: x in S ; ::_thesis: S is a_neighborhood of x reconsider V9 = V as non empty Subset of X by A2, Th4; consider S1 being Subset of (X | V) such that A5: S1 = S and A6: S1 is a_component by A3, CONNSP_1:def_6; consider V1 being Subset of X such that A7: V1 is a_neighborhood of x and A8: V1 is connected and A9: V1 c= V by A1, A2, Def3; V1 c= [#] (X | V) by A9, PRE_TOPC:def_5; then reconsider V2 = V1 as Subset of (X | V) ; A10: x in Int V1 by A7, Def1; V2 is connected by A8, CONNSP_1:23; then ( V2 misses S1 or V2 c= S1 ) by A6, CONNSP_1:36; then A11: ( V2 /\ S1 = {} (X | V9) or V2 c= S1 ) by XBOOLE_0:def_7; x in V2 by A7, Th4; then Int V1 c= Int S by A4, A5, A11, TOPS_1:19, XBOOLE_0:def_4; hence S is a_neighborhood of x by A10, Def1; ::_thesis: verum end; assume A12: for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x ; ::_thesis: X is_locally_connected_in x for U1 being Subset of X st U1 is a_neighborhood of x holds ex V being Subset of X st ( V is a_neighborhood of x & V is connected & V c= U1 ) proof let U1 be Subset of X; ::_thesis: ( U1 is a_neighborhood of x implies ex V being Subset of X st ( V is a_neighborhood of x & V is connected & V c= U1 ) ) A13: [#] (X | U1) = U1 by PRE_TOPC:def_5; assume A14: U1 is a_neighborhood of x ; ::_thesis: ex V being Subset of X st ( V is a_neighborhood of x & V is connected & V c= U1 ) then A15: x in U1 by Th4; reconsider U1 = U1 as non empty Subset of X by A14, Th4; x in [#] (X | U1) by A15, PRE_TOPC:def_5; then reconsider x1 = x as Point of (X | U1) ; set S1 = Component_of x1; reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11; take S ; ::_thesis: ( S is a_neighborhood of x & S is connected & S c= U1 ) Component_of x1 is a_component by CONNSP_1:40; then A16: S is_a_component_of U1 by CONNSP_1:def_6; ( x in S & Component_of x1 is connected ) by CONNSP_1:38; hence ( S is a_neighborhood of x & S is connected & S c= U1 ) by A12, A14, A13, A16, CONNSP_1:23; ::_thesis: verum end; hence X is_locally_connected_in x by Def3; ::_thesis: verum end; theorem Th14: :: CONNSP_2:14 for X being non empty TopSpace for x being Point of X holds ( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds ( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) let x be Point of X; ::_thesis: ( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) A1: ( X is_locally_connected_in x implies for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) proof assume A2: X is_locally_connected_in x ; ::_thesis: for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) let U1 be non empty Subset of X; ::_thesis: ( U1 is open & x in U1 implies ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) assume that A3: U1 is open and A4: x in U1 ; ::_thesis: ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) x in [#] (X | U1) by A4, PRE_TOPC:def_5; then reconsider x1 = x as Point of (X | U1) ; reconsider S1 = Component_of x1 as Subset of (X | U1) ; take x1 ; ::_thesis: ( x1 = x & x in Int (Component_of x1) ) reconsider S = S1 as Subset of X by PRE_TOPC:11; A5: x in S by CONNSP_1:38; S1 is a_component by CONNSP_1:40; then A6: S is_a_component_of U1 by CONNSP_1:def_6; U1 is a_neighborhood of x by A3, A4, Th3; then S is a_neighborhood of x by A2, A6, A5, Th13; then S1 is a_neighborhood of x1 by Th10; hence ( x1 = x & x in Int (Component_of x1) ) by Def1; ::_thesis: verum end; ( ( for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) implies X is_locally_connected_in x ) proof assume A7: for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ; ::_thesis: X is_locally_connected_in x for U1 being Subset of X st U1 is a_neighborhood of x holds ex V1 being Subset of X st ( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) proof let U1 be Subset of X; ::_thesis: ( U1 is a_neighborhood of x implies ex V1 being Subset of X st ( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) ) assume U1 is a_neighborhood of x ; ::_thesis: ex V1 being Subset of X st ( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) then consider V being non empty Subset of X such that A8: V is a_neighborhood of x and A9: V is open and A10: V c= U1 by Th5; consider x1 being Point of (X | V) such that A11: x1 = x and A12: x in Int (Component_of x1) by A7, A8, A9, Th4; set S1 = Component_of x1; reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11; take S ; ::_thesis: ( S is a_neighborhood of x & S is connected & S c= U1 ) Component_of x1 c= [#] (X | V) ; then A13: ( Component_of x1 is connected & S c= V ) by PRE_TOPC:def_5; Component_of x1 is a_neighborhood of x1 by A11, A12, Def1; hence ( S is a_neighborhood of x & S is connected & S c= U1 ) by A9, A10, A11, A13, Th9, CONNSP_1:23, XBOOLE_1:1; ::_thesis: verum end; hence X is_locally_connected_in x by Def3; ::_thesis: verum end; hence ( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) by A1; ::_thesis: verum end; theorem Th15: :: CONNSP_2:15 for X being non empty TopSpace st X is locally_connected holds for S being Subset of X st S is a_component holds S is open proof let X be non empty TopSpace; ::_thesis: ( X is locally_connected implies for S being Subset of X st S is a_component holds S is open ) assume A1: X is locally_connected ; ::_thesis: for S being Subset of X st S is a_component holds S is open let S be Subset of X; ::_thesis: ( S is a_component implies S is open ) assume A2: S is a_component ; ::_thesis: S is open now__::_thesis:_for_p_being_set_st_p_in_S_holds_ p_in_Int_S let p be set ; ::_thesis: ( p in S implies p in Int S ) assume A3: p in S ; ::_thesis: p in Int S then reconsider x = p as Point of X ; A4: [#] X is a_neighborhood of x by Th3; ( X is_locally_connected_in x & S is_a_component_of [#] X ) by A1, A2, Def4, Th11; then S is a_neighborhood of x by A3, A4, Th13; hence p in Int S by Def1; ::_thesis: verum end; then ( Int S c= S & S c= Int S ) by TARSKI:def_3, TOPS_1:16; then Int S = S by XBOOLE_0:def_10; hence S is open ; ::_thesis: verum end; theorem Th16: :: CONNSP_2:16 for X being non empty TopSpace for x being Point of X st X is_locally_connected_in x holds for A being non empty Subset of X st A is open & x in A holds A is_locally_connected_in x proof let X be non empty TopSpace; ::_thesis: for x being Point of X st X is_locally_connected_in x holds for A being non empty Subset of X st A is open & x in A holds A is_locally_connected_in x let x be Point of X; ::_thesis: ( X is_locally_connected_in x implies for A being non empty Subset of X st A is open & x in A holds A is_locally_connected_in x ) assume A1: X is_locally_connected_in x ; ::_thesis: for A being non empty Subset of X st A is open & x in A holds A is_locally_connected_in x let A be non empty Subset of X; ::_thesis: ( A is open & x in A implies A is_locally_connected_in x ) assume that A2: A is open and A3: x in A ; ::_thesis: A is_locally_connected_in x reconsider B = A as non empty Subset of X ; A4: [#] (X | A) = A by PRE_TOPC:def_5; for C being non empty Subset of X st B = C holds ex x1 being Point of (X | C) st ( x1 = x & X | C is_locally_connected_in x1 ) proof let C be non empty Subset of X; ::_thesis: ( B = C implies ex x1 being Point of (X | C) st ( x1 = x & X | C is_locally_connected_in x1 ) ) assume A5: B = C ; ::_thesis: ex x1 being Point of (X | C) st ( x1 = x & X | C is_locally_connected_in x1 ) then reconsider y = x as Point of (X | C) by A3, A4; take x1 = y; ::_thesis: ( x1 = x & X | C is_locally_connected_in x1 ) for U1 being Subset of (X | B) st U1 is a_neighborhood of x1 holds ex V being Subset of (X | B) st ( V is a_neighborhood of x1 & V is connected & V c= U1 ) proof let U1 be Subset of (X | B); ::_thesis: ( U1 is a_neighborhood of x1 implies ex V being Subset of (X | B) st ( V is a_neighborhood of x1 & V is connected & V c= U1 ) ) assume A6: U1 is a_neighborhood of x1 ; ::_thesis: ex V being Subset of (X | B) st ( V is a_neighborhood of x1 & V is connected & V c= U1 ) reconsider U2 = U1 as Subset of X by PRE_TOPC:11; U2 is a_neighborhood of x by A2, A5, A6, Th9; then consider V being Subset of X such that A7: ( V is a_neighborhood of x & V is connected ) and A8: V c= U2 by A1, Def3; reconsider V1 = V as Subset of (X | B) by A8, XBOOLE_1:1; take V1 ; ::_thesis: ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 ) thus ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 ) by A5, A7, A8, Th10, CONNSP_1:23; ::_thesis: verum end; hence ( x1 = x & X | C is_locally_connected_in x1 ) by A5, Def3; ::_thesis: verum end; hence A is_locally_connected_in x by Def5; ::_thesis: verum end; theorem Th17: :: CONNSP_2:17 for X being non empty TopSpace st X is locally_connected holds for A being non empty Subset of X st A is open holds A is locally_connected proof let X be non empty TopSpace; ::_thesis: ( X is locally_connected implies for A being non empty Subset of X st A is open holds A is locally_connected ) assume A1: X is locally_connected ; ::_thesis: for A being non empty Subset of X st A is open holds A is locally_connected let A be non empty Subset of X; ::_thesis: ( A is open implies A is locally_connected ) assume A2: A is open ; ::_thesis: A is locally_connected for x being Point of (X | A) holds X | A is_locally_connected_in x proof let x be Point of (X | A); ::_thesis: X | A is_locally_connected_in x x in [#] (X | A) ; then A3: x in A by PRE_TOPC:def_5; then reconsider x1 = x as Point of X ; X is_locally_connected_in x1 by A1, Def4; then A is_locally_connected_in x1 by A2, A3, Th16; then ex x2 being Point of (X | A) st ( x2 = x1 & X | A is_locally_connected_in x2 ) by Def5; hence X | A is_locally_connected_in x ; ::_thesis: verum end; then X | A is locally_connected by Def4; hence A is locally_connected by Def6; ::_thesis: verum end; theorem Th18: :: CONNSP_2:18 for X being non empty TopSpace holds ( X is locally_connected iff for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open ) proof let X be non empty TopSpace; ::_thesis: ( X is locally_connected iff for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open ) thus ( X is locally_connected implies for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open ) ::_thesis: ( ( for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open ) implies X is locally_connected ) proof assume A1: X is locally_connected ; ::_thesis: for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open let A be non empty Subset of X; ::_thesis: for B being Subset of X st A is open & B is_a_component_of A holds B is open let B be Subset of X; ::_thesis: ( A is open & B is_a_component_of A implies B is open ) assume that A2: A is open and A3: B is_a_component_of A ; ::_thesis: B is open consider B1 being Subset of (X | A) such that A4: B1 = B and A5: B1 is a_component by A3, CONNSP_1:def_6; reconsider B1 = B1 as Subset of (X | A) ; A is locally_connected by A1, A2, Th17; then X | A is locally_connected by Def6; then B1 is open by A5, Th15; then B1 in the topology of (X | A) by PRE_TOPC:def_2; then consider B2 being Subset of X such that A6: B2 in the topology of X and A7: B1 = B2 /\ ([#] (X | A)) by PRE_TOPC:def_4; A8: B = B2 /\ A by A4, A7, PRE_TOPC:def_5; reconsider B2 = B2 as Subset of X ; B2 is open by A6, PRE_TOPC:def_2; hence B is open by A2, A8; ::_thesis: verum end; assume A9: for A being non empty Subset of X for B being Subset of X st A is open & B is_a_component_of A holds B is open ; ::_thesis: X is locally_connected let x be Point of X; :: according to CONNSP_2:def_4 ::_thesis: X is_locally_connected_in x for U1 being non empty Subset of X st U1 is open & x in U1 holds ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) proof let U1 be non empty Subset of X; ::_thesis: ( U1 is open & x in U1 implies ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) ) assume that A10: U1 is open and A11: x in U1 ; ::_thesis: ex x1 being Point of (X | U1) st ( x1 = x & x in Int (Component_of x1) ) x in [#] (X | U1) by A11, PRE_TOPC:def_5; then reconsider x1 = x as Point of (X | U1) ; set S1 = Component_of x1; reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11; Component_of x1 is a_component by CONNSP_1:40; then S is_a_component_of U1 by CONNSP_1:def_6; then A12: S is open by A9, A10; take x1 ; ::_thesis: ( x1 = x & x in Int (Component_of x1) ) x in S by CONNSP_1:38; then Component_of x1 is a_neighborhood of x1 by A12, Th3, Th10; hence ( x1 = x & x in Int (Component_of x1) ) by Def1; ::_thesis: verum end; hence X is_locally_connected_in x by Th14; ::_thesis: verum end; theorem :: CONNSP_2:19 for X being non empty TopSpace st X is locally_connected holds for E being non empty Subset of X for C being non empty Subset of (X | E) st C is connected & C is open holds ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) proof let X be non empty TopSpace; ::_thesis: ( X is locally_connected implies for E being non empty Subset of X for C being non empty Subset of (X | E) st C is connected & C is open holds ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) ) assume A1: X is locally_connected ; ::_thesis: for E being non empty Subset of X for C being non empty Subset of (X | E) st C is connected & C is open holds ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) let E be non empty Subset of X; ::_thesis: for C being non empty Subset of (X | E) st C is connected & C is open holds ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) let C be non empty Subset of (X | E); ::_thesis: ( C is connected & C is open implies ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) ) assume that A2: C is connected and A3: C is open ; ::_thesis: ex H being Subset of X st ( H is open & H is connected & C = E /\ H ) C in the topology of (X | E) by A3, PRE_TOPC:def_2; then consider G being Subset of X such that A4: G in the topology of X and A5: C = G /\ ([#] (X | E)) by PRE_TOPC:def_4; A6: C = G /\ E by A5, PRE_TOPC:def_5; reconsider G = G as non empty Subset of X by A5; A7: G is open by A4, PRE_TOPC:def_2; reconsider C1 = C as Subset of X by PRE_TOPC:11; C <> {} (X | E) ; then consider x being Point of (X | E) such that A8: x in C by PRE_TOPC:12; x in G by A5, A8, XBOOLE_0:def_4; then x in [#] (X | G) by PRE_TOPC:def_5; then reconsider y = x as Point of (X | G) ; set H1 = Component_of y; reconsider H = Component_of y as Subset of X by PRE_TOPC:11; take H ; ::_thesis: ( H is open & H is connected & C = E /\ H ) A9: Component_of y is a_component by CONNSP_1:40; then H is_a_component_of G by CONNSP_1:def_6; hence H is open by A1, A7, Th18; ::_thesis: ( H is connected & C = E /\ H ) C c= G by A5, XBOOLE_1:17; then C c= [#] (X | G) by PRE_TOPC:def_5; then reconsider C2 = C1 as Subset of (X | G) ; Component_of y c= [#] (X | G) ; then A10: H c= G by PRE_TOPC:def_5; C1 is connected by A2, CONNSP_1:23; then C2 is connected by CONNSP_1:23; then ( C2 misses H or C2 c= H ) by A9, CONNSP_1:36; then A11: ( C2 /\ H = {} (X | G) or C2 c= H ) by XBOOLE_0:def_7; A12: x in Component_of y by CONNSP_1:38; then H /\ (G /\ E) c= C by A6, A8, A11, XBOOLE_0:def_4, XBOOLE_1:28; then (H /\ G) /\ E c= C by XBOOLE_1:16; then A13: E /\ H c= C by A10, XBOOLE_1:28; thus H is connected by CONNSP_1:23; ::_thesis: C = E /\ H C c= E by A6, XBOOLE_1:17; then C c= E /\ H by A8, A11, A12, XBOOLE_0:def_4, XBOOLE_1:19; hence C = E /\ H by A13, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th20: :: CONNSP_2:20 for X being non empty TopSpace holds ( X is normal iff for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ) proof let X be non empty TopSpace; ::_thesis: ( X is normal iff for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ) thus ( X is normal implies for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ) ::_thesis: ( ( for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ) implies X is normal ) proof assume A1: for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex G, H being Subset of X st ( G is open & H is open & A c= G & B c= H & G misses H ) ; :: according to COMPTS_1:def_3 ::_thesis: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) let A, C be Subset of X; ::_thesis: ( A <> {} & C <> [#] X & A c= C & A is closed & C is open implies ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ) assume that A2: A <> {} and A3: C <> [#] X and A4: A c= C and A5: A is closed and A6: C is open ; ::_thesis: ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) set B = ([#] X) \ C; ([#] X) \ C c= A ` by A4, XBOOLE_1:34; then A7: A misses ([#] X) \ C by SUBSET_1:23; ( ([#] X) \ C <> {} & C ` is closed ) by A3, A6, PRE_TOPC:4; then consider G, H being Subset of X such that A8: G is open and A9: H is open and A10: A c= G and A11: ([#] X) \ C c= H and A12: G misses H by A1, A2, A5, A7; take G ; ::_thesis: ( G is open & A c= G & Cl G c= C ) for p being set st p in Cl G holds p in C proof let p be set ; ::_thesis: ( p in Cl G implies p in C ) assume A13: p in Cl G ; ::_thesis: p in C then reconsider y = p as Point of X ; ( H ` is closed & G c= H ` ) by A9, A12, SUBSET_1:23; then A14: y in H ` by A13, PRE_TOPC:15; H ` c= (([#] X) \ C) ` by A11, SUBSET_1:12; then y in (([#] X) \ C) ` by A14; hence p in C by PRE_TOPC:3; ::_thesis: verum end; hence ( G is open & A c= G & Cl G c= C ) by A8, A10, TARSKI:def_3; ::_thesis: verum end; assume A15: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds ex G being Subset of X st ( G is open & A c= G & Cl G c= C ) ; ::_thesis: X is normal for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex G, H being Subset of X st ( G is open & H is open & A c= G & B c= H & G misses H ) proof let A, B be Subset of X; ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex G, H being Subset of X st ( G is open & H is open & A c= G & B c= H & G misses H ) ) assume that A16: A <> {} and A17: B <> {} and A18: A is closed and A19: ( B is closed & A misses B ) ; ::_thesis: ex G, H being Subset of X st ( G is open & H is open & A c= G & B c= H & G misses H ) set C = ([#] X) \ B; ([#] X) \ (([#] X) \ B) = B by PRE_TOPC:3; then A20: ([#] X) \ B <> [#] X by A17, PRE_TOPC:4; ( A c= B ` & ([#] X) \ B is open ) by A19, PRE_TOPC:def_3, SUBSET_1:23; then consider G being Subset of X such that A21: G is open and A22: A c= G and A23: Cl G c= ([#] X) \ B by A15, A16, A18, A20; take G ; ::_thesis: ex H being Subset of X st ( G is open & H is open & A c= G & B c= H & G misses H ) take H = ([#] X) \ (Cl G); ::_thesis: ( G is open & H is open & A c= G & B c= H & G misses H ) thus ( G is open & H is open ) by A21, PRE_TOPC:def_3; ::_thesis: ( A c= G & B c= H & G misses H ) (([#] X) \ B) ` c= (Cl G) ` by A23, SUBSET_1:12; hence ( A c= G & B c= H ) by A22, PRE_TOPC:3; ::_thesis: G misses H H c= G ` by PRE_TOPC:18, XBOOLE_1:34; hence G misses H by SUBSET_1:23; ::_thesis: verum end; hence X is normal by COMPTS_1:def_3; ::_thesis: verum end; theorem :: CONNSP_2:21 for X being non empty TopSpace st X is locally_connected & X is normal holds for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) proof let X be non empty TopSpace; ::_thesis: ( X is locally_connected & X is normal implies for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) ) assume that A1: X is locally_connected and A2: X is normal ; ::_thesis: for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) let A, B be Subset of X; ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected implies ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) ) assume that A3: A <> {} and A4: B <> {} and A5: A is closed and A6: ( B is closed & A misses B ) ; ::_thesis: ( not A is connected or not B is connected or ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) ) B = ([#] X) \ (([#] X) \ B) by PRE_TOPC:3; then A7: ([#] X) \ B <> [#] X by A4, PRE_TOPC:4; A <> {} X by A3; then consider x being Point of X such that A8: x in A by PRE_TOPC:12; ( A c= B ` & B ` is open ) by A6, SUBSET_1:23; then consider G being Subset of X such that A9: G is open and A10: A c= G and A11: Cl G c= B ` by A2, A3, A5, A7, Th20; A12: Cl G misses B by A11, SUBSET_1:23; A13: x in G by A10, A8; reconsider G = G as non empty Subset of X by A3, A10; x in [#] (X | G) by A13, PRE_TOPC:def_5; then reconsider y = x as Point of (X | G) ; A14: Cl G misses (Cl G) ` by XBOOLE_1:79; assume that A15: A is connected and A16: B is connected ; ::_thesis: ex R, S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) set H = Component_of y; reconsider H1 = Component_of y as Subset of X by PRE_TOPC:11; take R = H1; ::_thesis: ex S being Subset of X st ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) A17: Component_of y is a_component by CONNSP_1:40; then A18: H1 is_a_component_of G by CONNSP_1:def_6; A c= [#] (X | G) by A10, PRE_TOPC:def_5; then reconsider A1 = A as Subset of (X | G) ; A19: ( Component_of y is connected & y in Component_of y ) by CONNSP_1:38; A1 is connected by A15, CONNSP_1:23; then ( A1 misses Component_of y or A1 c= Component_of y ) by A17, CONNSP_1:36; then A20: ( A1 /\ (Component_of y) = {} or A1 c= Component_of y ) by XBOOLE_0:def_7; Component_of y c= [#] (X | G) ; then A21: R c= G by PRE_TOPC:def_5; G c= Cl G by PRE_TOPC:18; then A22: R c= Cl G by A21, XBOOLE_1:1; B <> {} X by A4; then consider z being Point of X such that A23: z in B by PRE_TOPC:12; A24: B c= (Cl G) ` by A12, SUBSET_1:23; then reconsider C = (Cl G) ` as non empty Subset of X by A23; z in (Cl G) ` by A23, A24; then z in [#] (X | C) by PRE_TOPC:def_5; then reconsider z1 = z as Point of (X | C) ; set V = Component_of z1; reconsider V1 = Component_of z1 as Subset of X by PRE_TOPC:11; take S = V1; ::_thesis: ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) A25: Component_of z1 is a_component by CONNSP_1:40; B c= [#] (X | ((Cl G) `)) by A24, PRE_TOPC:def_5; then reconsider B1 = B as Subset of (X | ((Cl G) `)) ; A26: ( Component_of z1 is connected & z1 in Component_of z1 ) by CONNSP_1:38; B1 is connected by A16, CONNSP_1:23; then ( B1 misses Component_of z1 or B1 c= Component_of z1 ) by A25, CONNSP_1:36; then A27: ( B1 /\ (Component_of z1) = {} or B1 c= Component_of z1 ) by XBOOLE_0:def_7; Component_of z1 c= [#] (X | ((Cl G) `)) ; then S c= (Cl G) ` by PRE_TOPC:def_5; then R /\ S c= (Cl G) /\ ((Cl G) `) by A22, XBOOLE_1:27; then R /\ S c= {} X by A14, XBOOLE_0:def_7; then A28: R /\ S = {} ; V1 is_a_component_of (Cl G) ` by A25, CONNSP_1:def_6; hence ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) by A1, A9, A8, A18, A20, A19, A23, A27, A26, A28, Th18, CONNSP_1:23, XBOOLE_0:def_4, XBOOLE_0:def_7; ::_thesis: verum end; theorem Th22: :: CONNSP_2:22 for X being non empty TopSpace for x being Point of X for F being Subset-Family of X st ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) holds F <> {} proof let X be non empty TopSpace; ::_thesis: for x being Point of X for F being Subset-Family of X st ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) holds F <> {} A1: ( [#] X is open & [#] X is closed ) ; let x be Point of X; ::_thesis: for F being Subset-Family of X st ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) holds F <> {} let F be Subset-Family of X; ::_thesis: ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) implies F <> {} ) assume for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ; ::_thesis: F <> {} hence F <> {} by A1; ::_thesis: verum end; definition let X be non empty TopSpace; let x be Point of X; func qComponent_of x -> Subset of X means :Def7: :: CONNSP_2:def 7 ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = it ); existence ex b1 being Subset of X ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b1 ) proof defpred S1[ set ] means ex A1 being Subset of X st ( A1 = \$1 & A1 is open & A1 is closed & x in \$1 ); consider F being Subset-Family of X such that A1: for A being Subset of X holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); reconsider S = meet F as Subset of X ; take S ; ::_thesis: ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S ) take F ; ::_thesis: ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S ) thus for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ::_thesis: meet F = S proof let A be Subset of X; ::_thesis: ( A in F iff ( A is open & A is closed & x in A ) ) thus ( A in F implies ( A is open & A is closed & x in A ) ) ::_thesis: ( A is open & A is closed & x in A implies A in F ) proof assume A in F ; ::_thesis: ( A is open & A is closed & x in A ) then ex A1 being Subset of X st ( A1 = A & A1 is open & A1 is closed & x in A ) by A1; hence ( A is open & A is closed & x in A ) ; ::_thesis: verum end; thus ( A is open & A is closed & x in A implies A in F ) by A1; ::_thesis: verum end; thus meet F = S ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of X st ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b1 ) & ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b2 ) holds b1 = b2 proof let S, S9 be Subset of X; ::_thesis: ( ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S ) & ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S9 ) implies S = S9 ) assume that A2: ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S ) and A3: ex F9 being Subset-Family of X st ( ( for A being Subset of X holds ( A in F9 iff ( A is open & A is closed & x in A ) ) ) & meet F9 = S9 ) ; ::_thesis: S = S9 consider F being Subset-Family of X such that A4: for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) and A5: meet F = S by A2; consider F9 being Subset-Family of X such that A6: for A being Subset of X holds ( A in F9 iff ( A is open & A is closed & x in A ) ) and A7: meet F9 = S9 by A3; A8: F9 <> {} by A6, Th22; A9: F <> {} by A4, Th22; now__::_thesis:_for_y_being_set_holds_ (_y_in_S_iff_y_in_S9_) let y be set ; ::_thesis: ( y in S iff y in S9 ) A10: now__::_thesis:_(_y_in_S9_implies_y_in_S_) assume A11: y in S9 ; ::_thesis: y in S for B being set st B in F holds y in B proof let B be set ; ::_thesis: ( B in F implies y in B ) assume A12: B in F ; ::_thesis: y in B then reconsider B1 = B as Subset of X ; ( B1 is open & B1 is closed & x in B1 ) by A4, A12; then B1 in F9 by A6; hence y in B by A7, A11, SETFAM_1:def_1; ::_thesis: verum end; hence y in S by A5, A9, SETFAM_1:def_1; ::_thesis: verum end; now__::_thesis:_(_y_in_S_implies_y_in_S9_) assume A13: y in S ; ::_thesis: y in S9 for B being set st B in F9 holds y in B proof let B be set ; ::_thesis: ( B in F9 implies y in B ) assume A14: B in F9 ; ::_thesis: y in B then reconsider B1 = B as Subset of X ; ( B1 is open & B1 is closed & x in B1 ) by A6, A14; then B1 in F by A4; hence y in B by A5, A13, SETFAM_1:def_1; ::_thesis: verum end; hence y in S9 by A7, A8, SETFAM_1:def_1; ::_thesis: verum end; hence ( y in S iff y in S9 ) by A10; ::_thesis: verum end; hence S = S9 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def7 defines qComponent_of CONNSP_2:def_7_:_ for X being non empty TopSpace for x being Point of X for b3 being Subset of X holds ( b3 = qComponent_of x iff ex F being Subset-Family of X st ( ( for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b3 ) ); theorem :: CONNSP_2:23 for X being non empty TopSpace for x being Point of X holds x in qComponent_of x proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds x in qComponent_of x let x be Point of X; ::_thesis: x in qComponent_of x consider F being Subset-Family of X such that A1: for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) and A2: qComponent_of x = meet F by Def7; ( F <> {} & ( for A being set st A in F holds x in A ) ) by A1, Th22; hence x in qComponent_of x by A2, SETFAM_1:def_1; ::_thesis: verum end; theorem :: CONNSP_2:24 for X being non empty TopSpace for x being Point of X for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds A = qComponent_of x proof let X be non empty TopSpace; ::_thesis: for x being Point of X for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds A = qComponent_of x let x be Point of X; ::_thesis: for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds A = qComponent_of x let A be Subset of X; ::_thesis: ( A is open & A is closed & x in A & A c= qComponent_of x implies A = qComponent_of x ) consider F being Subset-Family of X such that A1: for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) and A2: qComponent_of x = meet F by Def7; assume ( A is open & A is closed & x in A ) ; ::_thesis: ( not A c= qComponent_of x or A = qComponent_of x ) then A in F by A1; then A3: qComponent_of x c= A by A2, SETFAM_1:3; assume A c= qComponent_of x ; ::_thesis: A = qComponent_of x hence A = qComponent_of x by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CONNSP_2:25 for X being non empty TopSpace for x being Point of X holds qComponent_of x is closed proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds qComponent_of x is closed let x be Point of X; ::_thesis: qComponent_of x is closed consider F being Subset-Family of X such that A1: for A being Subset of X holds ( A in F iff ( A is open & A is closed & x in A ) ) and A2: qComponent_of x = meet F by Def7; for A being Subset of X st A in F holds A is closed by A1; hence qComponent_of x is closed by A2, PRE_TOPC:14; ::_thesis: verum end; theorem :: CONNSP_2:26 for X being non empty TopSpace for x being Point of X holds Component_of x c= qComponent_of x proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds Component_of x c= qComponent_of x let x be Point of X; ::_thesis: Component_of x c= qComponent_of x consider F9 being Subset-Family of X such that A1: for A being Subset of X holds ( A in F9 iff ( A is open & A is closed & x in A ) ) and A2: qComponent_of x = meet F9 by Def7; A3: for B1 being set st B1 in F9 holds Component_of x c= B1 proof set S = Component_of x; let B1 be set ; ::_thesis: ( B1 in F9 implies Component_of x c= B1 ) A4: x in Component_of x by CONNSP_1:38; assume A5: B1 in F9 ; ::_thesis: Component_of x c= B1 then reconsider B = B1 as Subset of X ; A6: x in B by A1, A5; A7: ( B is open & B is closed ) by A1, A5; then B ` is closed ; then Cl (B `) = B ` by PRE_TOPC:22; then A8: B misses Cl (B `) by XBOOLE_1:79; A9: ( (Component_of x) /\ B c= B & (Component_of x) /\ (B `) c= B ` ) by XBOOLE_1:17; Cl B = B by A7, PRE_TOPC:22; then Cl B misses B ` by XBOOLE_1:79; then B,B ` are_separated by A8, CONNSP_1:def_1; then A10: (Component_of x) /\ B,(Component_of x) /\ (B `) are_separated by A9, CONNSP_1:7; A11: [#] X = B \/ (B `) by PRE_TOPC:2; Component_of x = (Component_of x) /\ ([#] X) by XBOOLE_1:28 .= ((Component_of x) /\ B) \/ ((Component_of x) /\ (B `)) by A11, XBOOLE_1:23 ; then ( (Component_of x) /\ B = {} X or (Component_of x) /\ (B `) = {} X ) by A10, CONNSP_1:15; then Component_of x misses B ` by A6, A4, XBOOLE_0:def_4, XBOOLE_0:def_7; then Component_of x c= (B `) ` by SUBSET_1:23; hence Component_of x c= B1 ; ::_thesis: verum end; F9 <> {} by A1, Th22; hence Component_of x c= qComponent_of x by A2, A3, SETFAM_1:5; ::_thesis: verum end; theorem :: CONNSP_2:27 for T being non empty TopSpace for A being Subset of T for p being Point of T holds ( p in Cl A iff for G being a_neighborhood of p holds G meets A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for p being Point of T holds ( p in Cl A iff for G being a_neighborhood of p holds G meets A ) let A be Subset of T; ::_thesis: for p being Point of T holds ( p in Cl A iff for G being a_neighborhood of p holds G meets A ) let p be Point of T; ::_thesis: ( p in Cl A iff for G being a_neighborhood of p holds G meets A ) hereby ::_thesis: ( ( for G being a_neighborhood of p holds G meets A ) implies p in Cl A ) assume A1: p in Cl A ; ::_thesis: for G being a_neighborhood of p holds G meets A let G be a_neighborhood of p; ::_thesis: G meets A ( p in Int G & Int G is open ) by Def1; then A meets Int G by A1, PRE_TOPC:def_7; hence G meets A by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum end; assume A2: for G being a_neighborhood of p holds G meets A ; ::_thesis: p in Cl A now__::_thesis:_for_G_being_Subset_of_T_st_G_is_open_&_p_in_G_holds_ A_meets_G let G be Subset of T; ::_thesis: ( G is open & p in G implies A meets G ) assume ( G is open & p in G ) ; ::_thesis: A meets G then G is a_neighborhood of p by Th3; hence A meets G by A2; ::_thesis: verum end; hence p in Cl A by PRE_TOPC:def_7; ::_thesis: verum end; theorem :: CONNSP_2:28 for X being non empty TopSpace for A being Subset of X holds [#] X is a_neighborhood of A proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds [#] X is a_neighborhood of A let A be Subset of X; ::_thesis: [#] X is a_neighborhood of A Int ([#] X) = [#] X by TOPS_1:15; hence A c= Int ([#] X) ; :: according to CONNSP_2:def_2 ::_thesis: verum end; theorem :: CONNSP_2:29 for X being non empty TopSpace for A being Subset of X for Y being a_neighborhood of A holds A c= Y proof let X be non empty TopSpace; ::_thesis: for A being Subset of X for Y being a_neighborhood of A holds A c= Y let A be Subset of X; ::_thesis: for Y being a_neighborhood of A holds A c= Y let Y be a_neighborhood of A; ::_thesis: A c= Y ( A c= Int Y & Int Y c= Y ) by Def2, TOPS_1:16; hence A c= Y by XBOOLE_1:1; ::_thesis: verum end;