let x, y, z be Element of REAL ; :: thesis: real_dist . x,y <= (real_dist . x,z) + (real_dist . z,y)
A1: abs (x - y) <= (abs (x - z)) + (abs (z - y))

proof

abs (x - y) = abs ((x - z) + (z - y)) ;
hence abs (x - y) <= (abs (x - z)) + (abs (z - y)) by COMPLEX1:142; :: thesis: verum

end;

( real_dist . x,y = abs (x - y) & real_dist . x,z = abs (x - z) & real_dist . z,y = abs (z - y) ) by Def13;
hence real_dist . x,y <= (real_dist . x,z) + (real_dist . z,y) by A1; :: thesis: verum