theorem Th56: :: JORDAN2C:72

for n being Nat
for r being Real
for p, q being Point of (TOP-REAL n)
for u being Point of (Euclid n) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )