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:142;
( 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