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

proof

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } or A in bool the carrier of (TopSpaceMetr M) )
assume A in { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } ; :: thesis: A in bool the carrier of (TopSpaceMetr M)
then ex n being Element of 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 Element of NAT : n <> 0 } ) ; :: thesis: verum