theorem :: RUSUB_7:9

for X being RealUnitarySpace
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))