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;
A2: Balls x c= the topology of (TopSpaceMetr M)

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in Balls x ; :: thesis:
then consider n being Nat such that
A3: A = Ball (x9,(1 / n)) and
n <> 0 by A1;
Ball (x9,(1 / n)) in Family_open_set M by PCOMPS_1:29;
hence A in the topology of (TopSpaceMetr M) by A3, TOPMETR:12; :: thesis:

end;

let O be set ; :: thesis:
assume O in Balls x ; :: thesis:
then ex n being Nat st
( O = Ball (x9,(1 / n)) & n <> 0 ) by A1;
hence x in O by A1, GOBOARD6:1; :: thesis:

end;

A5: 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 Balls x & V c= O )

let O be Subset of (TopSpaceMetr M); :: thesis:
assume ( O is open & x in O ) ; :: thesis:
then consider r being Real such that
A6: r > 0 and
A7: Ball (x9,r) c= O by A1, TOPMETR:15;
reconsider r = r as Real ;
consider n being Nat such that
A8: 1 / n < r and
A9: n > 0 by A6, Lm1;
reconsider Ba = Ball (x9,(1 / n)) as Subset of (TopSpaceMetr M) by TOPMETR:12;
reconsider Ba = Ba as Subset of (TopSpaceMetr M) ;
take Ba ; :: thesis:
thus Ba in Balls x by A1, A9; :: thesis:
Ball (x9,(1 / n)) c= Ball (x9,r) by A8, PCOMPS_1:1;
hence Ba c= O by A7; :: thesis:

end;