let x, y be Real; :: thesis: |.(|.x.| - |.y.|).| <= |.x.| + |.y.|
( |.(|.x.| - |.y.|).| <= |.(x - y).| & |.(x - y).| <= |.x.| + |.y.| ) by COMPLEX1:57, COMPLEX1:64;
hence |.(|.x.| - |.y.|).| <= |.x.| + |.y.| by XXREAL_0:2; :: thesis: verum