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 )
assume x <> y ; :: thesis: 0 < dist x,y
then dist x,y <> 0 by METRIC_1:2;
hence 0 < dist x,y by METRIC_1:5; :: thesis: verum