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)

x in O

ex V being Subset of (TopSpaceMetr M) st

( V in Balls x & V c= O )

then Intersect (Balls x) = meet (Balls x) by SETFAM_1:def 9;

then x in Intersect (Balls x) by A10, A4, SETFAM_1:def 1;

hence ( Balls x is open & Balls x is x -quasi_basis ) by A2, A5, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum

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)

proof

A4:
for O being set st O in Balls x holds
let A be object ; :: 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 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: verum

end;assume A in Balls x ; :: thesis: A in the topology of (TopSpaceMetr M)

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: verum

x in O

proof

A5:
for O being Subset of (TopSpaceMetr M) st O is open & x in O holds
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 Nat st

( O = Ball (x9,(1 / n)) & n <> 0 ) by A1;

hence x in O by A1, GOBOARD6:1; :: thesis: verum

end;assume O in Balls x ; :: thesis: x in O

then ex n being Nat st

( O = Ball (x9,(1 / n)) & n <> 0 ) by A1;

hence x in O by A1, GOBOARD6:1; :: thesis: verum

ex V being Subset of (TopSpaceMetr M) st

( V in Balls x & V c= O )

proof

A10:
Ball (x9,(1 / 1)) in Balls x
by A1;
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 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: ( Ba in Balls x & Ba c= O )

thus Ba in Balls x by A1, A9; :: thesis: Ba c= O

Ball (x9,(1 / n)) c= Ball (x9,r) by A8, PCOMPS_1:1;

hence Ba c= O by A7; :: thesis: verum

end;( 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 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: ( Ba in Balls x & Ba c= O )

thus Ba in Balls x by A1, A9; :: thesis: Ba c= O

Ball (x9,(1 / n)) c= Ball (x9,r) by A8, PCOMPS_1:1;

hence Ba c= O by A7; :: thesis: verum

then Intersect (Balls x) = meet (Balls x) by SETFAM_1:def 9;

then x in Intersect (Balls x) by A10, A4, SETFAM_1:def 1;

hence ( Balls x is open & Balls x is x -quasi_basis ) by A2, A5, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum