let X be RealNormSpace; 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); 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; 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 A3:
{ y where y is Point of X : ||.(x - y).|| < r } c= { q where q is Element of (MetricSpaceNorm X) : dist (z,q) < 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 }
;
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; verum