let n be non zero Nat; :: thesis: for x, y being Element of REAL n holds (Infty_dist n) . (x,y) = (Infty_dist n) . (y,x)
let x, y be Element of REAL n; :: thesis: (Infty_dist n) . (x,y) = (Infty_dist n) . (y,x)
( (Infty_dist n) . (x,y) = sup (rng (abs (x - y))) & (Infty_dist n) . (y,x) = sup (rng (abs (y - x))) ) by Def7;
hence (Infty_dist n) . (x,y) = (Infty_dist n) . (y,x) by Th1; :: thesis: verum