for n being Element of NAT
for A being bounded Subset of (TOP-REAL n)
for a being Point of (TOP-REAL n) ex r being positive Real st A c= Ball (a,r)