let r, s, t be Real; :: thesis: ( r < s & s < t implies |.s.| < |.r.| + |.t.| )
assume that
A1: r < s and
A2: s < t ; :: thesis: |.s.| < |.r.| + |.t.|

per cases ( s < 0 or 0 <= s ) ;

suppose A3: s < 0 ; :: thesis: |.s.| < |.r.| + |.t.|

- s < - r by A1, XREAL_1:24;
then A4: (- s) + 0 < (- r) + |.t.| by COMPLEX1:46, XREAL_1:8;
- s = |.s.| by A3, ABSVALUE:def 1;
hence |.s.| < |.r.| + |.t.| by A1, A3, A4, ABSVALUE:def 1; :: thesis: verum

end;

suppose A5: 0 <= s ; :: thesis: |.s.| < |.r.| + |.t.|

A6: s + 0 < t + |.r.| by A2, COMPLEX1:46, XREAL_1:8;
s = |.s.| by A5, ABSVALUE:def 1;
hence |.s.| < |.r.| + |.t.| by A2, A5, A6, ABSVALUE:def 1; :: thesis: verum

end;

end;