let n be Nat; :: thesis: for R being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st R is connected & R is open & p in R & q in R & p <> q holds
ex f being Function of I[01],(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q )
let R be Subset of (TOP-REAL n); :: thesis: for p, q being Point of (TOP-REAL n) st R is connected & R is open & p in R & q in R & p <> q holds
ex f being Function of I[01],(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q )
let p, q be Point of (TOP-REAL n); :: thesis: ( R is connected & R is open & p in R & q in R & p <> q implies ex f being Function of I[01],(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) )
assume that
A1: ( R is connected & R is open & p in R ) and
A2: q in R and
A3: p <> q ; :: thesis: ex f being Function of I[01],(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q )
set RR = { q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } ;
{ q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } c= the carrier of (TOP-REAL n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } or x in the carrier of (TOP-REAL n) )
assume x in { q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex q2 being Point of (TOP-REAL n) st
( q2 = x & ( q2 = 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 = q2 ) ) ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then R c= { q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } by A1, Th62;
then q in { q2 where q2 is Point of (TOP-REAL n) : ( q2 = 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 = q2 ) ) } by A2;
then ex q2 being Point of (TOP-REAL n) st
( q = q2 & ( q2 = 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 = q2 ) ) ) ;
hence ex f being Function of I[01],(TOP-REAL n) st
( f is continuous & rng f c= R & f . 0 = p & f . 1 = q ) by A3; :: thesis: verum