theorem :: KURATO_2:7

for n being Nat
for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)