theorem Th8: :: NORMSP_2:8

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