theorem Th35: :: PCOMPS_1:35

for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )