MetricSpaceNorm N = MetrStruct(# the carrier of N,(distance_by_norm_of N) #) by NORMSP_2:def 2;
hence x is Element of N by Th9; :: thesis: verum