theorem Th1: :: METRIC_1:1

for M being MetrStruct holds
( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive )