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