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