let n be Element of NAT ; :: thesis: for B being non empty Subset of (TOP-REAL n) st B is open holds
(TOP-REAL n) | B is locally_connected
let B be non empty Subset of (TOP-REAL n); :: thesis: ( B is open implies (TOP-REAL n) | B is locally_connected )
assume A1: B is open ; :: thesis: (TOP-REAL n) | B is locally_connected
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
for A being non empty Subset of ((TOP-REAL n) | B)
for C being Subset of ((TOP-REAL n) | B) st A is open & C is_a_component_of A holds
C is open

proof

let A be non empty Subset of ((TOP-REAL n) | B); :: thesis: for C being Subset of ((TOP-REAL n) | B) st A is open & C is_a_component_of A holds
C is open
let C be Subset of ((TOP-REAL n) | B); :: thesis: ( A is open & C is_a_component_of A implies C is open )
assume A2: ( A is open & C is_a_component_of A ) ; :: thesis: C is open
then consider C1 being Subset of (((TOP-REAL n) | B) | A) such that
A3: ( C1 = C & C1 is_a_component_of ((TOP-REAL n) | B) | A ) by CONNSP_1:def 6;
A4: [#] ((TOP-REAL n) | B) = B by PRE_TOPC:def 10;
C1 c= [#] (((TOP-REAL n) | B) | A) ;
then A5: C1 c= A by PRE_TOPC:def 10;
A c= the carrier of ((TOP-REAL n) | B) ;
then A c= B by PRE_TOPC:29;
then C c= B by A3, A5, XBOOLE_1:1;
then reconsider C0 = C as Subset of (TOP-REAL n) by XBOOLE_1:1;
reconsider CC = C0 as Subset of (TopSpaceMetr (Euclid n)) by V;
for p being Point of (Euclid n) st p in C0 holds
ex r being real number st
( r > 0 & Ball p,r c= C0 )

proof

let p be Point of (Euclid n); :: thesis: ( p in C0 implies ex r being real number st
( r > 0 & Ball p,r c= C0 ) )
assume A6: p in C0 ; :: thesis: ex r being real number st
( r > 0 & Ball p,r c= C0 )
consider A0 being Subset of (TOP-REAL n) such that
A7: ( A0 is open & A0 /\ ([#] ((TOP-REAL n) | B)) = A ) by A2, TOPS_2:32;
A8: A0 /\ B = A by A7, PRE_TOPC:def 10;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider AA = A0 /\ B as Subset of (TopSpaceMetr (Euclid n)) by A8;
A0 /\ B is open by A1, A7, TOPS_1:38;
then AA is open by A2, V, PRE_TOPC:60;
then consider r1 being real number such that
A9: ( r1 > 0 & Ball p,r1 c= AA ) by A3, A5, A6, A8, TOPMETR:22;
reconsider r1 = r1 as Real by XREAL_0:def 1;
A10: ( r1 > 0 & Ball p,r1 c= A ) by A7, A9, PRE_TOPC:def 10;
reconsider BL1 = Ball p,r1 as Subset of (TOP-REAL n) by TOPREAL3:13;
reconsider BL1 = BL1 as Subset of (TOP-REAL n) ;
reconsider BL2 = Ball p,r1 as Subset of ((TOP-REAL n) | B) by A10, XBOOLE_1:1;
reconsider BL2 = BL2 as Subset of ((TOP-REAL n) | B) ;
Ball p,r1 c= [#] (((TOP-REAL n) | B) | A) by A10, PRE_TOPC:def 10;
then reconsider BL = Ball p,r1 as Subset of (((TOP-REAL n) | B) | A) ;
reconsider BL = BL as Subset of (((TOP-REAL n) | B) | A) ;

now

assume not Ball p,r1 c= C0 ; :: thesis: contradiction
then consider x being set such that
A11: ( x in Ball p,r1 & not x in C0 ) by TARSKI:def 3;
BL1 is convex by Th78;
then A12: BL2 is connected by Th15;
p in BL by A9, GOBOARD6:4;
then BL /\ C <> {} (((TOP-REAL n) | B) | A) by A6, XBOOLE_0:def 4;
then BL meets C by XBOOLE_0:def 7;
then BL c= C by A3, A12, Th15, CONNSP_1:38;
hence contradiction by A11; :: thesis: verum

end;

hence ex r being real number st
( r > 0 & Ball p,r c= C0 ) by A9; :: thesis: verum

end;

then CC is open by TOPMETR:22;
then A13: C0 is open by V, PRE_TOPC:60;
C c= the carrier of ((TOP-REAL n) | B) ;
then C c= B by PRE_TOPC:29;
then C0 /\ B = C by XBOOLE_1:28;
hence C is open by A4, A13, TOPS_2:32; :: thesis: verum

end;

hence (TOP-REAL n) | B is locally_connected by CONNSP_2:24; :: thesis: verum