let x, y, z be Element of REAL ; :: thesis: real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y))
abs (x - y) = abs ((x - z) + (z - y)) ;
then A1: abs (x - y) <= (abs (x - z)) + (abs (z - y)) by COMPLEX1:56;
( real_dist . (x,y) = abs (x - y) & real_dist . (x,z) = abs (x - z) ) by Def13;
hence real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y)) by A1, Def13; :: thesis: verum