let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for P, R being Subset of (TOP-REAL n) st 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
P c= R
let p be Point of (TOP-REAL n); :: thesis: for P, R being Subset of (TOP-REAL n) st 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
P c= R
let P, R be Subset of (TOP-REAL n); :: thesis: ( 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 P c= R )
assume that
A1: p in R and
A2: 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: P c= R
let x be object ; :: 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
A3: q = x and
A4: ( 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 ) ) by A2;

per cases ( 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 ) ) by A4;

suppose q = p ; :: thesis: x in R

hence x in R by A1, A3; :: thesis: verum

end;

suppose 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: x in R

then consider f1 being Function of I[01],(TOP-REAL n) such that
f1 is continuous and
A5: rng f1 c= R and
f1 . 0 = p and
A6: f1 . 1 = q ;
reconsider P1 = rng f1 as Subset of (TOP-REAL n) ;
dom f1 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then 1 in dom f1 by XXREAL_1:1;
then q in P1 by A6, FUNCT_1:def 3;
hence x in R by A3, A5; :: thesis: verum

end;

end;