:: deftheorem Def15 defines cl_Ball METRIC_1:def 15 :
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₄ = cl_Ball (p,r) iff b₄ = { q where q is Element of M : dist (p,q) <= r } ) ) & ( M is empty implies ( b₄ = cl_Ball (p,r) iff b₄ is empty ) ) );