:: deftheorem defines dist METRIC_1:def 1 :
for M being MetrStruct
for a, b being Element of M holds dist (a,b) = the distance of M . (a,b);