theorem Th23: :: METRIC_1:23

for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= (Empty^2-to-zero . (x,y)) + (Empty^2-to-zero . (y,z)) by Lm5;