let r0, s0, r, s be real number ; :: thesis: abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s))
(r0 - s0) - (r - s) = (r0 - r) - (s0 - s) ;
then A1: abs ((r0 - s0) - (r - s)) <= (abs (r0 - r)) + (abs (s0 - s)) by COMPLEX1:143;
abs ((abs (r0 - s0)) - (abs (r - s))) <= abs ((r0 - s0) - (r - s)) by COMPLEX1:150;
hence abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s)) by A1, XXREAL_0:2; :: thesis: verum