theorem Th11: :: METRIC_1:11

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