let M be non empty MetrSpace; :: thesis: for x being Point of (TopSpaceMetr M) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x))
let x be Point of (TopSpaceMetr M); :: thesis: Balls x is basis of (BOOL2F (NeighborhoodSystem x))
set F = BOOL2F (NeighborhoodSystem x);

now :: thesis: for t being object st t in Balls x holds
t in BOOL2F (NeighborhoodSystem x)

let t be object ; :: thesis: ( t in Balls x implies t in BOOL2F (NeighborhoodSystem x) )
assume A1: t in Balls x ; :: thesis: t in BOOL2F (NeighborhoodSystem x)
then reconsider t1 = t as Subset of (TopSpaceMetr M) ;
consider y being Point of M such that
A2: y = x and
A3: Balls x = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
consider n0 being Nat such that
A4: t = Ball (y,(1 / n0)) and
A5: n0 <> 0 by A1, A3;
reconsider r0 = 1 / n0 as Real ;
A6: 0 < r0 by A5;
dist (y,y) < r0 by A6, METRIC_1:1;
then A7: y in { q where q is Element of M : dist (y,q) < r0 } ;
( t1 is open & x in t1 ) by A7, A4, TOPMETR:14, A2, METRIC_1:def 14;
then t1 is a_neighborhood of x by CONNSP_2:3;
then t in NeighborhoodSystem x by YELLOW19:2;
hence t in BOOL2F (NeighborhoodSystem x) by CARDFIL2:def 20; :: thesis: verum

end;

then Balls x c= BOOL2F (NeighborhoodSystem x) ;
then reconsider BAX = Balls x as non empty Subset of (BOOL2F (NeighborhoodSystem x)) ;

now :: thesis: for f being Element of BOOL2F (NeighborhoodSystem x) ex b being Element of BAX st b c= f

let f be Element of BOOL2F (NeighborhoodSystem x); :: thesis: ex b being Element of BAX st b c= f
f in BOOL2F (NeighborhoodSystem x) ;
then f in NeighborhoodSystem x by CARDFIL2:def 20;
then f is a_neighborhood of x by YELLOW19:2;
then consider V being Subset of (TopSpaceMetr M) such that
A8: ( V is open & V c= f & x in V ) by CONNSP_2:6;
consider b being Subset of (TopSpaceMetr M) such that
A9: ( b in Balls x & b c= V ) by A8, YELLOW_8:def 1;
reconsider b = b as Element of BAX by A9;
take b = b; :: thesis: b c= f
thus b c= f by A8, A9; :: thesis: verum

end;

then BAX is filter_basis ;
hence Balls x is basis of (BOOL2F (NeighborhoodSystem x)) ; :: thesis: verum