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