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 10;
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:39;
U2 is
a_neighborhood of
x
by A2, A5, A6, Th11;
then consider V being
Subset of
X such that A7:
V is
a_neighborhood of
x
and A8:
V is
connected
and A9:
V c= U2
by A1, Def3;
reconsider V1 =
V as
Subset of
(X | B) by A9, 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, A9, Th12, CONNSP_1:24;
:: 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