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 18 :: 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 by Def2; :: 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 by Def2;
then for a, b being Element of M st a <> b holds
0 < dist a,b by Def1;
hence for a, b being Element of M st a <> b holds
0 < dist a,b ; :: thesis: verum