let x, y be real number ; :: thesis: abs ((abs x) - (abs y)) <= (abs x) + (abs y)
( abs ((abs x) - (abs y)) <= abs (x - y) & abs (x - y) <= (abs x) + (abs y) ) by COMPLEX1:57, COMPLEX1:64;
hence abs ((abs x) - (abs y)) <= (abs x) + (abs y) by XXREAL_0:2; :: thesis: verum