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_{1}( Nat) -> Element of K19( the carrier of M) = Ball (x9,(1 / M));

defpred S_{1}[ Nat] means M <> 0 ;

{ H_{1}(n) where n is Nat : S_{1}[n] } is countable
from CARD_4:sch 1();

hence Balls x is countable by A1; :: thesis: verum

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

defpred S

{ H

hence Balls x is countable by A1; :: thesis: verum