theorem Th13: :: TOPGEN_5:13

for n being Element of NAT
for a being Point of (TOP-REAL n)
for r being positive Real holds a in Ball (a,r)