theorem Th6: :: METRIC_1:6

for M being MetrStruct st ( for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) holds
M is MetrSpace