let x be Point of (); :: thesis: for y being Point of ()
for cB being basis of ()
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 () : dist (y,q) < 1 / n }

let y be Point of (); :: thesis: for cB being basis of ()
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 () : dist (y,q) < 1 / n }

let cB be basis of (); :: 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 () : 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 () : 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 () : dist (y,q) < 1 / n }
consider z being Point of () 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 () : dist (y,q) < 1 / n } by METRIC_1:def 14;
hence ex n being Nat st b = { q where q is Element of () : dist (y,q) < 1 / n } by A5, A1, A3; :: thesis: verum