let n be Nat; 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); 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); ( 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 ) ) }
; 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 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);
( 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
;
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;
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;
( r > 0 & Ball (u,r) c= P )thus
r > 0
by A10;
Ball (u,r) c= Preconsider r9 =
r as
Real ;
A12:
p2 in Ball (
u,
r9)
by A10, TBSP_1:11;
thus
Ball (
u,
r)
c= P
verum end;
then
P9 is open
by TOPMETR:15;
hence
P is open
by A4, PRE_TOPC:30; verum