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

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