for D being non empty set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty