let n be Element of NAT ; :: thesis:
let R be Subset of (TOP-REAL n); :: thesis:
let p be Point of (TOP-REAL n); :: thesis:
let P be Subset of (TOP-REAL n); :: thesis:
assume that
A1: ( R is connected & R is open ) and
A2: P = { q where q is Point of (TOP-REAL n) : ( q <> p & q in R & ( for f being Function of I[01] ,(TOP-REAL n) holds
( not f is continuous or not rng f c= R or not f . 0 = p or not f . 1 = q ) ) ) } ; :: thesis:
A3: 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)) ;
A4: P c= R

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in P ; :: thesis:
then ex q being Point of (TOP-REAL n) st
( q = x & q <> p & q in R & ( for f being Function of I[01] ,(TOP-REAL n) holds
( not f is continuous or not rng f c= R or not f . 0 = p or not f . 1 = q ) ) ) by A2;
hence x in R ; :: thesis:

end;

now

A5: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider R' = R as Subset of (TopSpaceMetr (Euclid n)) ;
let u be Point of (Euclid n); :: thesis:
reconsider p2 = u as Point of (TOP-REAL n) by TOPREAL3:13;
assume A6: u in P ; :: thesis:
R' is open by A1, A5, PRE_TOPC:60;
then consider r being real number such that
A7: r > 0 and
A8: Ball u,r c= R' by A4, A6, TOPMETR:22;
take r = r; :: thesis:
thus r > 0 by A7; :: thesis:
reconsider r' = r as Real by XREAL_0:def 1;
A9: p2 in Ball u,r' by A7, TBSP_1:16;
Ball u,r c= P'

assume not Ball u,r c= P' ; :: thesis:
then consider x being set such that
A10: x in Ball u,r and
A11: not x in P by TARSKI:def 3;
x in R by A8, A10;
then reconsider q = x as Point of (TOP-REAL n) ;

per cases by A2, A8, A10, A11;

suppose A12: q = p ; :: thesis:

A13: now

assume A14: q = p2 ; :: thesis:
ex p3 being Point of (TOP-REAL n) st
( p3 = p2 & p3 <> p & p3 in R & ( for f1 being Function of I[01] ,(TOP-REAL n) holds
( not f1 is continuous or not rng f1 c= R or not f1 . 0 = p or not f1 . 1 = p3 ) ) ) by A2, A6;
hence contradiction by A12, A14; :: thesis:

end;

u in Ball u,r' by A7, TBSP_1:16;
then A15: ex f2 being Function of I[01] ,(TOP-REAL n) st
( f2 is continuous & f2 . 0 = q & f2 . 1 = p2 & rng f2 c= Ball u,r' ) by A10, A13, Th80;
not p2 in P

assume p2 in P ; :: thesis:
then ex q4 being Point of (TOP-REAL n) st
( q4 = p2 & q4 <> p & q4 in R & ( for f1 being Function of I[01] ,(TOP-REAL n) holds
( not f1 is continuous or not rng f1 c= R or not f1 . 0 = p or not f1 . 1 = q4 ) ) ) by A2;
hence contradiction by A8, A12, A15, XBOOLE_1:1; :: thesis:

end;

hence contradiction by A6; :: thesis:

end;

suppose A16: ex f1 being Function of I[01] ,(TOP-REAL n) st
( f1 is continuous & rng f1 c= R & f1 . 0 = p & f1 . 1 = q ) ; :: thesis:

end;

hence contradiction by A6; :: thesis:

end;

hence Ball u,r c= P' ; :: thesis:

end;

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