theorem :: METRIC_1:18

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