theorem :: TOPREAL6:48

for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being Real st D = Ball (e,r) & p = e holds
N-bound D = (p `2) + r