let X be RealNormSpace; :: thesis: for z being Element of (MetricSpaceNorm X)

for r being Real ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

let z be Element of (MetricSpaceNorm X); :: thesis: for r being Real ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

let r be Real; :: thesis: ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

set M = MetricSpaceNorm X;

reconsider x = z as Point of X ;

A1: Ball (z,r) = { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by METRIC_1:def 14;

then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } = { y where y is Point of X : ||.(x - y).|| < r } by A3, XBOOLE_0:def 10;

hence ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } ) by A1; :: thesis: verum

for r being Real ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

let z be Element of (MetricSpaceNorm X); :: thesis: for r being Real ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

let r be Real; :: thesis: ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

set M = MetricSpaceNorm X;

reconsider x = z as Point of X ;

A1: Ball (z,r) = { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by METRIC_1:def 14;

now :: thesis: for a being object st a in { y where y is Point of X : ||.(x - y).|| < r } holds

a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }

then A3:
{ y where y is Point of X : ||.(x - y).|| < r } c= { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }
;a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }

let a be object ; :: thesis: ( a in { y where y is Point of X : ||.(x - y).|| < r } implies a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } )

assume a in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }

then consider y being Point of X such that

A2: ( a = y & ||.(x - y).|| < r ) ;

reconsider t = y as Element of (MetricSpaceNorm X) ;

||.(x - y).|| = dist (z,t) by Def1;

hence a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by A2; :: thesis: verum

end;assume a in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r }

then consider y being Point of X such that

A2: ( a = y & ||.(x - y).|| < r ) ;

reconsider t = y as Element of (MetricSpaceNorm X) ;

||.(x - y).|| = dist (z,t) by Def1;

hence a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } by A2; :: thesis: verum

now :: thesis: for a being object st a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } holds

a in { y where y is Point of X : ||.(x - y).|| < r }

then
{ q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } c= { y where y is Point of X : ||.(x - y).|| < r }
;a in { y where y is Point of X : ||.(x - y).|| < r }

let a be object ; :: thesis: ( a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } implies a in { y where y is Point of X : ||.(x - y).|| < r } )

assume a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } ; :: thesis: a in { y where y is Point of X : ||.(x - y).|| < r }

then consider q being Element of (MetricSpaceNorm X) such that

A4: ( a = q & dist (z,q) < r ) ;

reconsider t = q as Point of X ;

||.(x - t).|| = dist (z,q) by Def1;

hence a in { y where y is Point of X : ||.(x - y).|| < r } by A4; :: thesis: verum

end;assume a in { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } ; :: thesis: a in { y where y is Point of X : ||.(x - y).|| < r }

then consider q being Element of (MetricSpaceNorm X) such that

A4: ( a = q & dist (z,q) < r ) ;

reconsider t = q as Point of X ;

||.(x - t).|| = dist (z,q) by Def1;

hence a in { y where y is Point of X : ||.(x - y).|| < r } by A4; :: thesis: verum

then { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < r } = { y where y is Point of X : ||.(x - y).|| < r } by A3, XBOOLE_0:def 10;

hence ex x being Point of X st

( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } ) by A1; :: thesis: verum