:: deftheorem Def8 defines symmetric METRIC_1:def 8 :
for M being MetrStruct holds
( M is symmetric iff the distance of M is symmetric );