let r1, r2, r3, r4 be Real; :: thesis: abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4))
r2 - r4 = (r2 - r3) + (r3 - r4) ;
then abs (r2 - r4) <= (abs (r2 - r3)) + (abs (r3 - r4)) by COMPLEX1:56;
then A1: (abs (r1 - r2)) + (abs (r2 - r4)) <= (abs (r1 - r2)) + ((abs (r2 - r3)) + (abs (r3 - r4))) by XREAL_1:7;
r1 - r4 = (r1 - r2) + (r2 - r4) ;
then abs (r1 - r4) <= (abs (r1 - r2)) + (abs (r2 - r4)) by COMPLEX1:56;
hence abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4)) by A1, XXREAL_0:2; :: thesis: verum