theorem Th60: :: JORDAN2C:76
for n being Nat
for p being Point of (TOP-REAL n)
for R, P being Subset 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
P is open