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
consider V1 being
Subset of
X such that A5:
V1 is
a_neighborhood of
x
and A6:
V1 is
connected
and A7:
V1 c= V
by A1, A2, Def3;
consider S1 being
Subset of
(X | V) such that A8:
(
S1 = S &
S1 is_a_component_of X | V )
by A3, CONNSP_1:def 6;
reconsider V' =
V as non
empty Subset of
X by A2, Th6;
V1 c= [#] (X | V)
by A7, PRE_TOPC:def 10;
then reconsider V2 =
V1 as
Subset of
(X | V) ;
V2 is
connected
by A6, CONNSP_1:24;
then
(
V2 misses S1 or
V2 c= S1 )
by A8, CONNSP_1:38;
then A9:
(
V2 /\ S1 = {} (X | V') or
V2 c= S1 )
by XBOOLE_0:def 7;
(
x in V2 &
x in S1 )
by A4, A5, A8, Th6;
then A10:
Int V1 c= Int S
by A8, A9, TOPS_1:48, XBOOLE_0:def 4;
x in Int V1
by A5, Def1;
hence
S is
a_neighborhood of
x
by A10, Def1;
:: thesis: verum
end;
assume A11:
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 )
hence
X is_locally_connected_in x
by Def3; :: thesis: verum