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 3 :: 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 by Def7; :: 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 by Def7;
hence for a being Element of M holds dist a,a = 0 by Def3; :: thesis: verum