let X be RealUnitarySpace; :: thesis: for z being Element of (MetricSpaceNorm (RUSp2RNSp X))
for r being Real ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
let z be Element of (MetricSpaceNorm (RUSp2RNSp X)); :: thesis: for r being Real ex x being Point of X st
( x = z & cl_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 & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )
reconsider x = z as Point of X ;
set M = MetricSpaceNorm (RUSp2RNSp X);
A1: cl_Ball (z,r) = { q where q is Element of (MetricSpaceNorm (RUSp2RNSp X)) : dist (z,q) <= r } by METRIC_1:def 15;
A3: { y where y is Point of X : ||.(x - y).|| <= r } c= { q where q is Element of (MetricSpaceNorm (RUSp2RNSp X)) : dist (z,q) <= r }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Point of X : ||.(x - y).|| <= r } or a in { q where q is Element of (MetricSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp 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 (RUSp2RNSp X)) ;
||.(x - y).|| = dist (z,t) by Th1;
hence a in { q where q is Element of (MetricSpaceNorm (RUSp2RNSp X)) : dist (z,q) <= r } by A2; :: thesis: verum

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { q where q is Element of (MetricSpaceNorm (RUSp2RNSp X)) : dist (z,q) <= r } or a in { y where y is Point of X : ||.(x - y).|| <= r } )
assume a in { q where q is Element of (MetricSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp X)) such that
A4: ( a = q & dist (z,q) <= r ) ;
reconsider t = q as Point of X ;
||.(x - t).|| = dist (z,q) by Th1;
hence a in { y where y is Point of X : ||.(x - y).|| <= r } by A4; :: thesis: verum

end;

then { q where q is Element of (MetricSpaceNorm (RUSp2RNSp X)) : dist (z,q) <= r } = { y where y is Point of X : ||.(x - y).|| <= r } by A3;
hence ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } ) by A1; :: thesis: verum