set B = Balls x;
consider x9 being Point of M such that
A1: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1;
deffunc H₁( Element of NAT ) -> Element of K10( the carrier of M) = Ball (x9,(1 / M));
defpred S₁[ Element of NAT ] means M <> 0 ;
{ H₁(n) where n is Element of NAT : S₁[n] } is countable from CARD_4:sch 1();
hence Balls x is countable by A1; :: thesis: verum