A1: the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12;
then reconsider y = x as Point of M ;
set B = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ;
{ (Ball (y,(1 / n))) where n is Nat : n <> 0 } c= bool the carrier of (TopSpaceMetr M)

proof

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { (Ball (y,(1 / n))) where n is Nat : n <> 0 } or A in bool the carrier of (TopSpaceMetr M) )
assume A in { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ; :: thesis: A in bool the carrier of (TopSpaceMetr M)
then ex n being Nat st
( A = Ball (y,(1 / n)) & n <> 0 ) ;
hence A in bool the carrier of (TopSpaceMetr M) by A1; :: thesis: verum

end;

hence ex b₁ being Subset-Family of (TopSpaceMetr M) ex y being Point of M st
( y = x & b₁ = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) ; :: thesis: verum