theorem :: TOPREAL6:46

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
E-bound D = (p `1) + r