let n be 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))
let x, y, z be Element of REAL n; (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))
( (Infty_dist n) . (x,y) in REAL & (Infty_dist n) . (x,z) in REAL & (Infty_dist n) . (z,y) in REAL )
;
then reconsider sxy = sup (rng (abs (x - y))), sxz = sup (rng (abs (x - z))), szy = sup (rng (abs (z - y))) as Real by Def7;
sxy <= sxz + szy
then
sxy <= sxz + ((Infty_dist n) . (z,y))
by Def7;
then
sxy <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))
by Def7;
hence
(Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))
by Def7; verum