theorem Th12: :: METRIC_1:12

for r being Real
for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )