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 )

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

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

end;0 < dist (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 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;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

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