let x, y be real number ; :: thesis: abs ((abs x) - (abs y)) <= (abs x) + (abs y)
A1: abs ((abs x) - (abs y)) <= abs (x - y) by COMPLEX1:150;
abs (x - y) <= (abs x) + (abs y) by COMPLEX1:143;
hence abs ((abs x) - (abs y)) <= (abs x) + (abs y) by A1, XXREAL_0:2; :: thesis: verum