let X be RealNormSpace; :: thesis: for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
let x be Point of X; :: thesis: for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
let r be Real; :: thesis: { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)
reconsider z = x as Element of (MetricSpaceNorm X) ;
ex t being Point of X st
( t = x & cl_Ball (z,r) = { y where y is Point of X : ||.(t - y).|| <= r } ) by Th3;
hence { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X) by TOPREAL6:57; :: thesis: verum