for n being non zero Nat
for x, y, z being Element of REAL n holds (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))