let n be 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 :: thesis: for u being Point of (Euclid n) st u in P9 holds
ex r being Real st
( r > 0 & Ball (u,r) c= P )

let u be Point of (Euclid n); :: thesis: ( u in P9 implies ex r being Real st
( r > 0 & Ball (u,r) c= P ) )
reconsider p2 = u as Point of (TOP-REAL n) by TOPREAL3:8;
assume u in P9 ; :: thesis: ex r being Real 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 :: thesis: p2 in R

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:40, FUNCT_2:def 1;
then 1 in dom f2 by XXREAL_1:1;
then u in rng f2 by A5, A9, FUNCT_1:def 3;
hence p2 in R by A8; :: thesis: verum

end;

end;

end;

RR is open by A1, A4, PRE_TOPC:30;
then consider r being Real such that
A10: r > 0 and
A11: Ball (u,r) c= R by A7, TOPMETR:15;
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 ;
A12: p2 in Ball (u,r9) by A10, TBSP_1:11;
thus Ball (u,r) c= P :: thesis: verum

proof

let x be object ; :: 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 :: thesis: ( q1 = p implies x in P )

assume q1 = p ; :: thesis: x in P
then p in Ball (u,r9) by A5, A10, TBSP_1:11;
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, Th56;
rng f2 c= R by A11, A17;
hence x in P by A3, A16; :: thesis: verum

end;

now :: thesis: ( q1 <> p implies x in P )

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, Th58;
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:15;
hence P is open by A4, PRE_TOPC:30; :: thesis: verum