:: deftheorem Def6 defines Reflexive METRIC_1:def 6 :
for M being MetrStruct holds
( M is Reflexive iff the distance of M is Reflexive );