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
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P' = P as Subset of (TopSpaceMetr (Euclid n)) by XX, YY;
reconsider RR = R as Subset of (TopSpaceMetr (Euclid n)) by V;

now

let u be Point of (Euclid n); :: thesis: ( u in P' 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 P' ; :: 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
A4: q1 = u and
A5: ( 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;
X: RR is open by V, A1, PRE_TOPC:60;

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 A5;

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

hence p2 in R by A2, A4; :: 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
A6: ( rng f2 c= R & f2 . 0 = p & 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 A4, A6, FUNCT_1:def 5;
hence p2 in R by A6; :: thesis: verum

end;

end;

end;

then consider r being real number such that
A7: ( r > 0 & Ball u,r c= R ) by A1, X, TOPMETR:22;
reconsider r' = r as Real by XREAL_0:def 1;
A8: p2 in Ball u,r' by A7, TBSP_1:16;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A7; :: thesis: Ball u,r c= P
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 A9: x in Ball u,r ; :: thesis: x in P
then reconsider q = x as Point of (TOP-REAL n) by A7, 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 A10: q <> p ; :: thesis: x in P

A11: 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 A4, A5, A7, A8, A9, Th82;
hence x in P by A3; :: thesis: verum

end;

now

assume q1 = p ; :: thesis: x in P
then p in Ball u,r' by A4, A7, TBSP_1:16;
then consider f2 being Function of I[01] ,(TOP-REAL n) such that
A12: ( f2 is continuous & f2 . 0 = p & f2 . 1 = q & rng f2 c= Ball u,r' ) by A9, A10, Th80;
( f2 is continuous & rng f2 c= R & f2 . 0 = p & f2 . 1 = q ) by A7, A12, XBOOLE_1:1;
hence x in P by A3; :: thesis: verum

end;

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

end;

end;

end;

end;

then P' is open by TOPMETR:22;
hence P is open by V, PRE_TOPC:60; :: thesis: verum