theorem :: CARDFIL4:69

for x being Point of (TopSpaceMetr (Euclid 1))
for y being Point of (Euclid 1)
for cB being basis of (BOOL2F (NeighborhoodSystem x))
for b being Element of cB st x = y & cB = Balls x holds
ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }