for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M)
for x9 being Point of M st x = x9 holds
ex f being sequence of (Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))