let n be non zero Nat; :: thesis: Infty_dist n is_metric_of REAL n
for x, y, z being Element of REAL n holds
( ( (Infty_dist n) . (x,y) = 0 implies x = y ) & ( x = y implies (Infty_dist n) . (x,y) = 0 ) & (Infty_dist n) . (x,y) = (Infty_dist n) . (y,x) & (Infty_dist n) . (x,z) <= ((Infty_dist n) . (x,y)) + ((Infty_dist n) . (y,z)) ) by Th59, Th60, Th61;
hence Infty_dist n is_metric_of REAL n by PCOMPS_1:def 6; :: thesis: verum