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