let n be 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 R9 = R as non empty Subset of (TOP-REAL n) by A2;
A4: p in P by A3;
set P2 = R \ P;
reconsider P22 = R \ P as Subset of (TOP-REAL n) ;
A5: [#] ((TOP-REAL n) | R) = R by PRE_TOPC:def 5;
then reconsider P11 = P, P12 = P22 as Subset of ((TOP-REAL n) | R) by A2, A3, Th61, XBOOLE_1:36;
reconsider P11 = P11, P12 = P12 as Subset of ((TOP-REAL n) | R) ;
P \/ (R \ P) = P \/ R by XBOOLE_1:39;
then A6: ( P11 misses P12 & [#] ((TOP-REAL n) | R) = P11 \/ P12 ) by A5, XBOOLE_1:12, XBOOLE_1:79;

now :: thesis: for x being object holds
( x in R \ P iff x in { 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 ) ) ) } )

let x be object ; :: thesis: ( x in R \ P iff x in { 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 ) ) ) } )

A7: now :: thesis: ( x in R \ P implies x in { 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 ) ) ) } )

assume A8: x in R \ P ; :: thesis: x in { 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 ) ) ) }
then reconsider q2 = x as Point of (TOP-REAL n) ;
not x in P by A8, XBOOLE_0:def 5;
then A9: ( q2 <> p & ( 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 = q2 ) ) ) by A3;
q2 in R by A8, XBOOLE_0:def 5;
hence x in { 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 A9; :: thesis: verum

end;

now :: thesis: ( x in { 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 x in R \ P )

assume x in { 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: x in R \ P
then A10: ex q3 being Point of (TOP-REAL n) st
( q3 = x & q3 <> p & q3 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 = q3 ) ) ) ;
then for q being Point of (TOP-REAL n) holds
( not q = x or ( not q = p & ( 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 ) ) ) ) ;
then not x in P by A3;
hence x in R \ P by A10, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x in R \ P iff x in { 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 A7; :: thesis: verum

end;

then 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;
then P22 is open by A1, Th59;
then A11: P22 in the topology of (TOP-REAL n) by PRE_TOPC:def 2;
reconsider PPP = P as Subset of (TOP-REAL n) ;
PPP is open by A1, A2, A3, Th60;
then A12: P in the topology of (TOP-REAL n) by PRE_TOPC:def 2;
P11 = P /\ ([#] ((TOP-REAL n) | R)) by XBOOLE_1:28;
then P11 in the topology of ((TOP-REAL n) | R) by A12, PRE_TOPC:def 4;
then A13: P11 is open by PRE_TOPC:def 2;
P12 = P22 /\ ([#] ((TOP-REAL n) | R)) by XBOOLE_1:28;
then P12 in the topology of ((TOP-REAL n) | R) by A11, PRE_TOPC:def 4;
then A14: P12 is open by PRE_TOPC:def 2;
(TOP-REAL n) | R9 is connected by A1, CONNSP_1:def 3;
then ( P11 = {} ((TOP-REAL n) | R) or P12 = {} ((TOP-REAL n) | R) ) by A6, A13, A14, CONNSP_1:11;
hence R c= P by A4, XBOOLE_1:37; :: thesis: verum