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