let n be Element of NAT ; :: thesis: for P, R being Subset of (TOP-REAL n)
for p being Point 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
R c= P
let P, R be Subset of (TOP-REAL n); :: thesis: for p being Point 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
R c= P
let p be Point of (TOP-REAL n); :: thesis: ( 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 R c= P )
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 ) ) }
; :: thesis: R c= P
reconsider R' = R as non empty Subset of (TOP-REAL n) by A2;
set P2 = R \ P;
then A8:
R \ 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 ) ) ) }
by TARSKI:2;
reconsider P22 = R \ P as Subset of (TOP-REAL n) ;
A9:
P22 is open
by A1, A8, Th83;
reconsider PPP = P as Subset of (TOP-REAL n) ;
A10:
PPP is open
by A1, A2, A3, Th84;
A11:
p in P
by A3;
A12:
(TOP-REAL n) | R' is connected
by A1, CONNSP_1:def 3;
A13:
[#] ((TOP-REAL n) | R) = R
by PRE_TOPC:def 10;
then reconsider P11 = P, P12 = P22 as Subset of ((TOP-REAL n) | R) by A2, A3, Th85, XBOOLE_1:36;
reconsider P11 = P11, P12 = P12 as Subset of ((TOP-REAL n) | R) ;
A14:
P11 misses P12
by XBOOLE_1:79;
P \/ (R \ P) = P \/ R
by XBOOLE_1:39;
then A15:
[#] ((TOP-REAL n) | R) = P11 \/ P12
by A13, XBOOLE_1:12;
A16:
( P22 in the topology of (TOP-REAL n) & P in the topology of (TOP-REAL n) )
by A9, A10, PRE_TOPC:def 5;
( P11 = P /\ ([#] ((TOP-REAL n) | R)) & P12 = P22 /\ ([#] ((TOP-REAL n) | R)) )
by XBOOLE_1:28;
then
( P11 in the topology of ((TOP-REAL n) | R) & P12 in the topology of ((TOP-REAL n) | R) )
by A16, PRE_TOPC:def 9;
then
( P11 is open & P12 is open )
by PRE_TOPC:def 5;
then
( P11 = {} ((TOP-REAL n) | R) or P12 = {} ((TOP-REAL n) | R) )
by A12, A14, A15, CONNSP_1:12;
hence
R c= P
by A11, XBOOLE_1:37; :: thesis: verum