let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL n)
for R, P being Subset of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) ) } holds
P is open
let p be Point of (TOP-REAL n); :: thesis: for R, P being Subset of (TOP-REAL n) st R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) ) } holds
P is open
let R, P be Subset of (TOP-REAL n); :: thesis: ( R is connected & R is open & p in R & P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) ) } implies P is open )
assume that
A1: ( R is connected & R is open ) and
A2: p in R and
A3: P = { q where q is Point of (TOP-REAL n) : ( q = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) ) } ; :: thesis: P is open
A4: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P9 = P as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider RR = R as Subset of (TopSpaceMetr (Euclid n)) by A4;

now

let u be Point of (Euclid n); :: thesis: ( u in P9 implies ex r being real number st
( r > 0 & Ball u,r c= P ) )
reconsider p2 = u as Point of (TOP-REAL n) by TOPREAL3:13;
assume u in P9 ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P )
then consider q1 being Point of (TOP-REAL n) such that
A5: q1 = u and
A6: ( q1 = p or ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q1 ) ) by A3;

A7: now

per cases ( q1 = p or ( q1 <> p & ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q1 ) ) ) by A6;

suppose q1 = p ; :: thesis: p2 in R

hence p2 in R by A2, A5; :: thesis: verum

end;

suppose ( q1 <> p & ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q1 ) ) ; :: thesis: p2 in R

then consider f2 being Function of I[01] ,(TOP-REAL n) such that
f2 is continuous and
A8: rng f2 c= R and
f2 . 0 = p and
A9: f2 . 1 = q1 ;
dom f2 = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then 1 in dom f2 by XXREAL_1:1;
then u in rng f2 by A5, A9, FUNCT_1:def 5;
hence p2 in R by A8; :: thesis: verum

end;

end;

end;

RR is open by A1, A4, PRE_TOPC:60;
then consider r being real number such that
A10: r > 0 and
A11: Ball u,r c= R by A7, TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A10; :: thesis: Ball u,r c= P
reconsider r9 = r as Real by XREAL_0:def 1;
A12: p2 in Ball u,r9 by A10, TBSP_1:16;
thus Ball u,r c= P :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball u,r or x in P )
assume A13: x in Ball u,r ; :: thesis: x in P
then reconsider q = x as Point of (TOP-REAL n) by A11, TARSKI:def 3;

per cases ( q = p or q <> p ) ;

suppose q = p ; :: thesis: x in P

hence x in P by A3; :: thesis: verum

end;

suppose A14: q <> p ; :: thesis: x in P

A15: now

assume q1 = p ; :: thesis: x in P
then p in Ball u,r9 by A5, A10, TBSP_1:16;
then consider f2 being Function of I[01] ,(TOP-REAL n) such that
A16: ( f2 is continuous & f2 . 0 = p & f2 . 1 = q ) and
A17: rng f2 c= Ball u,r9 by A13, A14, Th80;
rng f2 c= R by A11, A17, XBOOLE_1:1;
hence x in P by A3, A16; :: thesis: verum

end;

now

assume q1 <> p ; :: thesis: x in P
then ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) by A5, A6, A11, A12, A13, Th82;
hence x in P by A3; :: thesis: verum

end;

hence x in P by A15; :: thesis: verum

end;

end;

end;

end;

then P9 is open by TOPMETR:22;
hence P is open by A4, PRE_TOPC:60; :: thesis: verum