let x, y be R_eal; :: thesis: ( ( x is Real or y is Real ) implies |.(|.x.| - |.y.|).| <= |.(x - y).| )
assume A1: ( x is Real or y is Real ) ; :: thesis: |.(|.x.| - |.y.|).| <= |.(x - y).|
then A2: |.x.| - |.y.| <= |.(x - y).| by Th68;
A3: |.y.| - |.x.| <= |.(y - x).| by A1, Th68;
y - x = - (x - y) by XXREAL_3:27;
then A4: |.(y - x).| = |.(x - y).| by Th66;
|.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:27;
then - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A3, A4, XXREAL_3:40;
hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A2, Th60; :: thesis: verum