let M be MetrStruct ; :: thesis: ( ( for a, b being Element of M st dist (a,b) = 0 holds

a = b ) iff M is discerning )

a = b

then the distance of M is discerning ;

hence for a, b being Element of M st dist (a,b) = 0 holds

a = b ; :: thesis: verum

a = b ) iff M is discerning )

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

a = b )

assume
M is discerning
; :: thesis: for a, b being Element of M st dist (a,b) = 0 holds a = b )

assume A1:
for a, b being Element of M st dist (a,b) = 0 holds

a = b ; :: thesis: M is discerning

the distance of M is discerning

end;a = b ; :: thesis: M is discerning

the distance of M is discerning

proof

hence
M is discerning
; :: thesis: verum
let a, b be Element of M; :: according to METRIC_1:def 3 :: thesis: ( the distance of M . (a,b) = 0 implies a = b )

assume the distance of M . (a,b) = 0 ; :: thesis: a = b

then dist (a,b) = 0 ;

hence a = b by A1; :: thesis: verum

end;assume the distance of M . (a,b) = 0 ; :: thesis: a = b

then dist (a,b) = 0 ;

hence a = b by A1; :: thesis: verum

a = b

then the distance of M is discerning ;

hence for a, b being Element of M st dist (a,b) = 0 holds

a = b ; :: thesis: verum