set B = Balls x;
consider x9 being Point of M such that
A0: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def10;
A2: Balls x c= the topology of (TopSpaceMetr M)

proof

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

end;

A5: for O being set st O in Balls x holds
x in O

proof

let O be set ; :: thesis: ( O in Balls x implies x in O )
assume O in Balls x ; :: thesis: x in O
then ex n being Element of NAT st
( O = Ball (x9,(1 / n)) & n <> 0 ) by A0;
hence x in O by A0, GOBOARD6:4; :: thesis: verum

end;

A6: 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 )

proof

let O be Subset of (TopSpaceMetr M); :: thesis: ( O is open & x in O implies ex V being Subset of (TopSpaceMetr M) st
( V in Balls x & V c= O ) )
assume ( O is open & x in O ) ; :: thesis: ex V being Subset of (TopSpaceMetr M) st
( V in Balls x & V c= O )
then consider r being real number such that
A7: r > 0 and
A8: Ball (x9,r) c= O by A0, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
consider n being Element of NAT such that
A9: 1 / n < r and
A10: n > 0 by A7, Lm1;
reconsider Ba = Ball (x9,(1 / n)) as Subset of (TopSpaceMetr M) by TOPMETR:16;
reconsider Ba = Ba as Subset of (TopSpaceMetr M) ;
take Ba ; :: thesis: ( Ba in Balls x & Ba c= O )
thus Ba in Balls x by A0, A10; :: thesis: Ba c= O
Ball (x9,(1 / n)) c= Ball (x9,r) by A9, PCOMPS_1:1;
hence Ba c= O by A8, XBOOLE_1:1; :: thesis: verum

end;

A11: Ball (x9,(1 / 1)) in Balls x by A0;
then Intersect (Balls x) = meet (Balls x) by SETFAM_1:def 10;
then x in Intersect (Balls x) by A11, A5, SETFAM_1:def 1;
hence ( Balls x is open & Balls x is x -quasi_basis ) by A2, A6, TOPS_2:78, YELLOW_8:def 2; :: thesis: verum