:: deftheorem defines MetricSpaceNorm NORMSP_2:def 2 :
for X being RealNormSpace holds MetricSpaceNorm X = MetrStruct(# the carrier of X,(distance_by_norm_of X) #);