let M be MetrStruct ; :: thesis: ( ( for a, b being Element of M st dist (a,b) = 0 holds
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 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

proof

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;

hence M is discerning ; :: thesis: verum

end;

assume M is discerning ; :: thesis: for a, b being Element of M st dist (a,b) = 0 holds
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