theorem Th31: :: JORDAN1K:31

for r being Real
for y being Point of (Euclid 2) st y = |[0,0]| holds
Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.q.| < r }