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