theorem :: RUSUB_7:8

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 open Subset of (TopSpaceNorm (RUSp2RNSp X))