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: 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 consider q being Point of (TOP-REAL n) such that
A4: ( 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;
thus x in R by A4; :: thesis: verum

end;

reconsider P' = P as Subset of (TopSpaceMetr (Euclid n)) ;

now

let u be Point of (Euclid n); :: thesis: ( u in P implies ex r being real number st
( r > 0 & Ball u,r c= P' ) )
reconsider p2 = u as Point of (TOP-REAL n) by TOPREAL3:13;
assume A5: u in P ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P' )
reconsider R' = R as Subset of (TopSpaceMetr (Euclid n)) ;
consider r being real number such that
A6: ( r > 0 & Ball u,r c= R' ) by A1, A3, A5, TOPMETR:22;
reconsider r' = r as Real by XREAL_0:def 1;
A7: p2 in Ball u,r' by A6, TBSP_1:16;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P' )
thus r > 0 by A6; :: thesis: Ball u,r c= P'
Ball u,r c= P'

proof

assume not Ball u,r c= P' ; :: thesis: contradiction
then consider x being set such that
A8: ( x in Ball u,r & not x in P ) by TARSKI:def 3;
x in R by A6, A8;
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, A6, A8;

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

now

assume A10: 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, A5;
hence contradiction by A9, A10; :: thesis: verum

end;

then ( q <> p2 & u in Ball u,r' ) by A6, TBSP_1:16;
then consider f2 being Function of I[01] ,(TOP-REAL n) such that
A11: ( f2 is continuous & f2 . 0 = q & f2 . 1 = p2 & rng f2 c= Ball u,r' ) by A8, 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 A6, A9, A11, XBOOLE_1:1; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

suppose A12: 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 A6, A7, A8, A12, Th82; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

end;

end;

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

end;

hence P is open by TOPMETR:22; :: thesis: verum