theorem Th3: :: KURATO_2:3

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 - p9).| < r holds
x in Ball (p,r)