let D be non empty set ; :: thesis: for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty
let f be Function of [:D,D:],REAL; :: thesis: ( f is_metric_of D implies not SpaceMetr (D,f) is empty )
assume f is_metric_of D ; :: thesis: not SpaceMetr (D,f) is empty
then SpaceMetr (D,f) = MetrStruct(# D,f #) by Def7;
hence not SpaceMetr (D,f) is empty ; :: thesis: verum