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

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

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

then A2: ( - s = abs s & - r = abs r ) by A1, ABSVALUE:def 1;
- s < - r by A1, XREAL_1:26;
then (- s) + 0 < (- r) + (abs t) by COMPLEX1:132, XREAL_1:10;
hence abs s < (abs r) + (abs t) by A2; :: thesis: verum

end;

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

then A3: ( s = abs s & t = abs t ) by A1, ABSVALUE:def 1;
s + 0 < t + (abs r) by A1, COMPLEX1:132, XREAL_1:10;
hence abs s < (abs r) + (abs t) by A3; :: thesis: verum

end;

end;