theorem Th18: :: TOPDIM_2:18

for U being Point of (TOP-REAL 1)
for r, u1 being Real st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}