theorem Th2: :: JGRAPH_2:2

for n being Element of NAT
for q2 being Point of (Euclid n)
for q being Point of (TOP-REAL n)
for r being Real st q = q2 holds
Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }