:: deftheorem defines TopSpaceNorm NORMSP_2:def 3 :
for X being RealNormSpace holds TopSpaceNorm X = TopSpaceMetr (MetricSpaceNorm X);