let X be RealNormSpace; :: thesis: for z being Element of (MetricSpaceNorm X)
for r being real number 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 number 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 number ; :: thesis: ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )
reconsider x = z as Point of X ;
consider M9 being non empty MetrStruct , z9 being Element of M9 such that
A1: M9 = MetricSpaceNorm X and
A2: z9 = z and
A3: Ball (z,r) = { q where q is Element of M9 : dist (z9,q) < r } by METRIC_1:def 14;

now

let a be set ; :: thesis: ( a in { y where y is Point of X : ||.(x - y).|| < r } implies a in { q where q is Element of M9 : dist (z9,q) < r } )
assume a in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: a in { q where q is Element of M9 : dist (z9,q) < r }
then consider y being Point of X such that
A4: ( a = y & ||.(x - y).|| < r ) ;
reconsider t = y as Element of M9 by A1;
||.(x - y).|| = dist (z9,t) by A1, A2, Def1;
hence a in { q where q is Element of M9 : dist (z9,q) < r } by A4; :: thesis: verum

end;

then A5: { y where y is Point of X : ||.(x - y).|| < r } c= { q where q is Element of M9 : dist (z9,q) < r } by TARSKI:def 3;

now

let a be set ; :: thesis: ( a in { q where q is Element of M9 : dist (z9,q) < r } implies a in { y where y is Point of X : ||.(x - y).|| < r } )
assume a in { q where q is Element of M9 : dist (z9,q) < r } ; :: thesis: a in { y where y is Point of X : ||.(x - y).|| < r }
then consider q being Element of M9 such that
A6: ( a = q & dist (z9,q) < r ) ;
reconsider t = q as Point of X by A1;
||.(x - t).|| = dist (z9,q) by A1, A2, Def1;
hence a in { y where y is Point of X : ||.(x - y).|| < r } by A6; :: thesis: verum

end;

then { q where q is Element of M9 : dist (z9,q) < r } c= { y where y is Point of X : ||.(x - y).|| < r } by TARSKI:def 3;
then { q where q is Element of M9 : dist (z9,q) < r } = { y where y is Point of X : ||.(x - y).|| < r } by A5, 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 A3; :: thesis: verum