:: deftheorem defines Reflexive METRIC_1:def 2 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is Reflexive iff for a being Element of A holds f . (a,a) = 0 );