theorem Th4: :: METRIC_1:4

for M being MetrStruct holds
( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle )