let M be non empty MetrStruct ; :: thesis: ( ( for a, b being Element of M st a <> b holds
0 < dist (a,b) ) iff M is Discerning )

hereby :: thesis: ( M is Discerning implies for a, b being Element of M st a <> b holds
0 < dist (a,b) )

assume A1: for a, b being Element of M st a <> b holds
0 < dist (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 17 :: thesis: ( a <> b implies 0 < the distance of M . (a,b) )
assume a <> b ; :: thesis: 0 < the distance of M . (a,b)
then 0 < dist (a,b) by A1;
hence 0 < the distance of M . (a,b) ; :: thesis: verum

end;

hence M is Discerning ; :: thesis: verum

end;

assume M is Discerning ; :: thesis: for a, b being Element of M st a <> b holds
0 < dist (a,b)
then the distance of M is Discerning ;
hence for a, b being Element of M st a <> b holds
0 < dist (a,b) ; :: thesis: verum