:: deftheorem Def7 defines SpaceMetr PCOMPS_1:def 7 :
for D being set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
SpaceMetr (D,f) = MetrStruct(# D,f #);