theorem Th2: :: KURATO_2:2

for n being Nat
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r