( the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric & the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle ) by Lm1, Lm2, Lm3, Lm4;
hence MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is non empty MetrSpace by METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9, METRIC_1:def 10; :: thesis: verum