let M be MetrSpace; :: thesis: for x, y being Element of M st x <> y holds
0 < dist (x,y)
let x, y be Element of M; :: thesis: ( x <> y implies 0 < dist (x,y) )
A1: dist (x,y) >= 0 by Th5;
assume x <> y ; :: thesis: 0 < dist (x,y)
then dist (x,y) <> 0 by Th2;
hence 0 < dist (x,y) by A1, XXREAL_0:1; :: thesis: verum