for x, y, z being Element of REAL holds real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y))