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