theorem :: METRIC_1:17

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