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