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)_{1} being Subset-Family of (TopSpaceMetr M) ex y being Point of M st

( y = x & b_{1} = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )
; :: thesis: verum

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

hence
ex b
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;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

( y = x & b