let r, s, r0, s0 be Real; :: thesis: |.(|.(r0 - s0).| - |.(r - s).|).| <= |.(r0 - r).| + |.(s0 - s).|
(r0 - s0) - (r - s) = (r0 - r) - (s0 - s) ;
then A1: |.((r0 - s0) - (r - s)).| <= |.(r0 - r).| + |.(s0 - s).| by COMPLEX1:57;
|.(|.(r0 - s0).| - |.(r - s).|).| <= |.((r0 - s0) - (r - s)).| by COMPLEX1:64;
hence |.(|.(r0 - s0).| - |.(r - s).|).| <= |.(r0 - r).| + |.(s0 - s).| by A1, XXREAL_0:2; :: thesis: verum