:: deftheorem Def9 defines triangle METRIC_1:def 9 :
for M being MetrStruct holds
( M is triangle iff the distance of M is triangle );