let X be RealUnitarySpace; :: 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 (RUSp2RNSp 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 (RUSp2RNSp X))
let r be Real; :: thesis: { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm (RUSp2RNSp X))
reconsider z = x as Element of (MetricSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp X)) by TOPREAL6:57; :: thesis: verum