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

then the distance of M is Reflexive ;

hence for a being Element of M holds dist (a,a) = 0 ; :: thesis: verum

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

assume
M is Reflexive
; :: thesis: 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

end;the distance of M is Reflexive

proof

hence
M is Reflexive
; :: thesis: verum
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;the distance of M . (a,a) = dist (a,a)

.= 0 by A1 ;

hence the distance of M . (a,a) = 0 ; :: thesis: verum

then the distance of M is Reflexive ;

hence for a being Element of M holds dist (a,a) = 0 ; :: thesis: verum