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