let N be RealNormSpace; :: thesis: for x being Point of (TopSpaceMetr (MetricSpaceNorm N))
for y being Point of (MetricSpaceNorm N)
for n being positive Nat st x = y holds
Ball (y,(1 / n)) in Balls x
let x be Point of (TopSpaceMetr (MetricSpaceNorm N)); :: thesis: for y being Point of (MetricSpaceNorm N)
for n being positive Nat st x = y holds
Ball (y,(1 / n)) in Balls x
let y be Point of (MetricSpaceNorm N); :: thesis: for n being positive Nat st x = y holds
Ball (y,(1 / n)) in Balls x
let n be positive Nat; :: thesis: ( x = y implies Ball (y,(1 / n)) in Balls x )
assume A1: x = y ; :: thesis: Ball (y,(1 / n)) in Balls x
set M = MetricSpaceNorm N;
consider y1 being Point of (MetricSpaceNorm N) such that
A2: y1 = x and
A3: Balls x = { (Ball (y1,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
thus Ball (y,(1 / n)) in Balls x by A1, A2, A3; :: thesis: verum