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);

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

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

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)

then
Balls x c= BOOL2F (NeighborhoodSystem x)
;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;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

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

then
BAX is filter_basis
;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;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

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