let M be non empty Reflexive Discerning MetrStruct ; :: thesis: for a, b being Element of M holds 0 <= dist (a,b)

let a, b be Element of M; :: thesis: 0 <= dist (a,b)

hence 0 <= dist (a,b) ; :: thesis: verum

let a, b be Element of M; :: thesis: 0 <= dist (a,b)

hence 0 <= dist (a,b) ; :: thesis: verum