let x be Point of (TopSpaceMetr (Euclid 1)); :: thesis: for y being Point of (Euclid 1)

for cB being basis of (BOOL2F (NeighborhoodSystem x))

for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let y be Point of (Euclid 1); :: thesis: for cB being basis of (BOOL2F (NeighborhoodSystem x))

for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let b be Element of cB; :: thesis: ( x = y & cB = Balls x implies ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } )

assume that

A1: x = y and

A2: cB = Balls x ; :: thesis: ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

consider z being Point of (Euclid 1) such that

A3: x = z and

A4: Balls x = { (Ball (z,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

b in { (Ball (z,(1 / n))) where n is Nat : n <> 0 } by A2, A4;

then consider n being Nat such that

A5: b = Ball (z,(1 / n)) and

n <> 0 ;

Ball (y,(1 / n)) = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } by METRIC_1:def 14;

hence ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } by A5, A1, A3; :: thesis: verum

for cB being basis of (BOOL2F (NeighborhoodSystem x))

for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let y be Point of (Euclid 1); :: thesis: for cB being basis of (BOOL2F (NeighborhoodSystem x))

for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: for b being Element of cB st x = y & cB = Balls x holds

ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

let b be Element of cB; :: thesis: ( x = y & cB = Balls x implies ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } )

assume that

A1: x = y and

A2: cB = Balls x ; :: thesis: ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n }

consider z being Point of (Euclid 1) such that

A3: x = z and

A4: Balls x = { (Ball (z,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

b in { (Ball (z,(1 / n))) where n is Nat : n <> 0 } by A2, A4;

then consider n being Nat such that

A5: b = Ball (z,(1 / n)) and

n <> 0 ;

Ball (y,(1 / n)) = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } by METRIC_1:def 14;

hence ex n being Nat st b = { q where q is Element of (Euclid 1) : dist (y,q) < 1 / n } by A5, A1, A3; :: thesis: verum