let n be 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 P9 = P as Subset of (TopSpaceMetr (Euclid n)) ;
A4: P c= R

let x be object ; :: 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;

A5: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider R9 = 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:8;
assume A6: u in P ; :: thesis:
R9 is open by A1, A5, PRE_TOPC:30;
then consider r being Real such that
A7: r > 0 and
A8: Ball (u,r) c= R9 by A4, A6, TOPMETR:15;
take r = r; :: thesis:
thus r > 0 by A7; :: thesis:
reconsider r9 = r as Real ;
A9: p2 in Ball (u,r9) by A7, TBSP_1:11;
Ball (u,r) c= P9

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

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;

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;

end;

end;

end;

hence Ball (u,r) c= P9 ; :: thesis:

end;