theorem Th5: :: METRIC_1:5

for M being Reflexive symmetric triangle MetrStruct
for a, b being Element of M holds 0 <= dist (a,b)