theorem :: METRIC_1:19

for r being Real
for M being non empty MetrStruct
for p being Element of M holds Sphere (p,r) = { q where q is Element of M : dist (p,q) = r } by Def16;