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; :: thesis: verum
end;
hence X is_locally_connected_in x ; :: 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