let M be MetrStruct ; :: thesis: ( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive )

hereby :: thesis: ( M is Reflexive implies for a being Element of M holds dist (a,a) = 0 )

assume A1: for a being Element of M holds dist (a,a) = 0 ; :: thesis: M is Reflexive
the distance of M is Reflexive

proof

let a be Element of M; :: according to METRIC_1:def 2 :: thesis: the distance of M . (a,a) = 0
the distance of M . (a,a) = dist (a,a)
.= 0 by A1 ;
hence the distance of M . (a,a) = 0 ; :: thesis: verum

end;

hence M is Reflexive ; :: thesis: verum

end;

assume M is Reflexive ; :: thesis: for a being Element of M holds dist (a,a) = 0
then the distance of M is Reflexive ;
hence for a being Element of M holds dist (a,a) = 0 ; :: thesis: verum