:: deftheorem Def14 defines Ball METRIC_1:def 14 :
for M being MetrStruct
for p being Element of M
for r being Real
for b₄ being Subset of M holds
( ( not M is empty implies ( b₄ = Ball (p,r) iff b₄ = { q where q is Element of M : dist (p,q) < r } ) ) & ( M is empty implies ( b₄ = Ball (p,r) iff b₄ is empty ) ) );