theorem Th30: :: METRIC_3:30

for x, y, z being Element of [:REAL,REAL,REAL:] holds Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z))