let r, s, t be real number ; :: thesis: ( r < s & s < t implies abs s < (abs r) + (abs t) )
assume that
A1: r < s and
A2: s < t ; :: thesis: abs s < (abs r) + (abs t)

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

suppose A3: s < 0 ; :: thesis: abs s < (abs r) + (abs t)

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

end;

suppose A5: 0 <= s ; :: thesis: abs s < (abs r) + (abs t)

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

end;

end;