let n be Element of NAT ; :: thesis: for R being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st R is connected & R is open & 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 ) ) ) } holds
P is open
let R be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st R is connected & R is open & 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 ) ) ) } holds
P is open
let p be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st R is connected & R is open & 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 ) ) ) } holds
P is open
let P be Subset of (TOP-REAL n); :: thesis: ( R is connected & R is open & 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 ) ) ) } implies P is open )
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: P is open
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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in R )
assume x in P ; :: thesis: x in R
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: verum

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 R9 = R as Subset of (TopSpaceMetr (Euclid n)) ;
let u be Point of (Euclid n); :: thesis: ( u in P implies ex r being real number st
( r > 0 & Ball u,r c= P9 ) )
reconsider p2 = u as Point of (TOP-REAL n) by TOPREAL3:13;
assume A6: u in P ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P9 )
R9 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= R9 by A4, A6, TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P9 )
thus r > 0 by A7; :: thesis: Ball u,r c= P9
reconsider r9 = r as Real by XREAL_0:def 1;
A9: p2 in Ball u,r9 by A7, TBSP_1:16;
Ball u,r c= P9

proof

assume not Ball u,r c= P9 ; :: thesis: contradiction
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 ( q = p or ex f1 being Function of I[01] ,(TOP-REAL n) st
( f1 is continuous & rng f1 c= R & f1 . 0 = p & f1 . 1 = q ) ) by A2, A8, A10, A11;

suppose A12: q = p ; :: thesis: contradiction

A13: now

assume A14: q = p2 ; :: thesis: contradiction
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: verum

end;

u in Ball u,r9 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,r9 ) by A10, A13, Th80;
not p2 in P

proof

assume p2 in P ; :: thesis: contradiction
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: verum

end;

hence contradiction by A6; :: thesis: verum

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: contradiction

not p2 in P

proof

assume p2 in P ; :: thesis: contradiction
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, A9, A10, A16, Th82; :: thesis: verum

end;

hence contradiction by A6; :: thesis: verum

end;

end;

end;

hence Ball u,r c= P9 ; :: thesis: verum

end;

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