theorem :: TOPREAL6:52

for a being Real
for X being non empty compact Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))