let M be non empty MetrSpace; :: thesis:
let x be Point of (TopSpaceMetr M); :: thesis:
let x' be Point of M; :: thesis:
assume A1: x = x' ; :: thesis:
set B = { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } ;
{ (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } c= bool the carrier of (TopSpaceMetr M)

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } ; :: thesis:
then consider n being Element of NAT such that
A2: A = Ball x',(1 / n) and
n <> 0 ;
Ball x',(1 / n) c= the carrier of M ;
then Ball x',(1 / n) c= the carrier of (TopSpaceMetr M) by TOPMETR:16;
hence A in bool the carrier of (TopSpaceMetr M) by A2; :: thesis:

end;

then reconsider B = { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } as Subset-Family of (TopSpaceMetr M) ;
A3: B c= the topology of (TopSpaceMetr M)

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in B ; :: thesis:
then consider n being Element of NAT such that
A4: A = Ball x',(1 / n) and
n <> 0 ;
Ball x',(1 / n) in Family_open_set M by PCOMPS_1:33;
hence A in the topology of (TopSpaceMetr M) by A4, TOPMETR:16; :: thesis:

end;

A5: x in Intersect B

A6: Ball x',(1 / 1) in B ;
then A7: Intersect B = meet B by SETFAM_1:def 10;
for O being set st O in B holds
x in O

let O be set ; :: thesis:
assume O in B ; :: thesis:
then consider n being Element of NAT such that
A8: O = Ball x',(1 / n) and
A9: n <> 0 ;
thus x in O by A1, A8, A9, GOBOARD6:4; :: thesis:

end;

hence x in Intersect B by A6, A7, SETFAM_1:def 1; :: thesis:

end;

for O being Subset of (TopSpaceMetr M) st O is open & x in O holds
ex V being Subset of (TopSpaceMetr M) st
( V in B & V c= O )

let O be Subset of (TopSpaceMetr M); :: thesis:
assume ( O is open & x in O ) ; :: thesis:
then consider r being real number such that
A10: r > 0 and
A11: Ball x',r c= O by A1, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
consider n being Element of NAT such that
A12: 1 / n < r and
A13: n > 0 by A10, Lm2;
A14: Ball x',(1 / n) c= Ball x',r by A12, PCOMPS_1:1;
reconsider Ba = Ball x',(1 / n) as Subset of (TopSpaceMetr M) by TOPMETR:16;
reconsider Ba = Ba as Subset of (TopSpaceMetr M) ;
take Ba ; :: thesis:
thus Ba in B by A13; :: thesis:
thus Ba c= O by A11, A14, XBOOLE_1:1; :: thesis:

end;

then reconsider B = B as Basis of x by A3, A5, YELLOW_8:def 2;
take B ; :: thesis:
deffunc H₁( Element of NAT ) -> Element of K10(the carrier of M) = Ball x',(1 / $1);
defpred S₁[ Element of NAT ] means $1 <> 0 ;
thus B = { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } ; :: thesis:
{ H₁(n) where n is Element of NAT : S₁[n] } is countable from CARD_4:sch 1();
hence B is countable ; :: thesis:
defpred S₂[ set , set ] means ex n' being Element of NAT st
( $1 = n' & $2 = Ball x',(1 / (n' + 1)) );
A15: for n being set st n in NAT holds
ex O being set st
( O in B & S₂[n,O] )

let n be set ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n' = n as Element of NAT ;
reconsider O = Ball x',(1 / (n' + 1)) as set ;
take O ; :: thesis:
thus O in B ; :: thesis:
take n' ; :: thesis:
thus n = n' ; :: thesis:
thus O = Ball x',(1 / (n' + 1)) ; :: thesis:

end;

consider f being Function such that
A16: dom f = NAT and
A17: rng f c= B and
A18: for n being set st n in NAT holds
S₂[n,f . n] from WELLORD2:sch 1(A15);
reconsider f = f as Function of NAT ,B by A16, A17, FUNCT_2:4;
take f ; :: thesis:
thus for n being set st n in NAT holds
ex n' being Element of NAT st
( n = n' & f . n = Ball x',(1 / (n' + 1)) ) by A18; :: thesis: