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 Def8;
hence not SpaceMetr D,f is empty ; :: thesis: verum