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

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