let x, y be ExtReal; :: thesis: ( ( x is Real or y is Real ) implies |.(|.x.| - |.y.|).| <= |.(x - y).| )
A1: |.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:26;
assume A2: ( x is Real or y is Real ) ; :: thesis: |.(|.x.| - |.y.|).| <= |.(x - y).|
then A3: |.x.| - |.y.| <= |.(x - y).| by Th20;
y - x = - (x - y) by XXREAL_3:26;
then A4: |.(y - x).| = |.(x - y).| by Th18;
|.y.| - |.x.| <= |.(y - x).| by A2, Th20;
then - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A4, A1, XXREAL_3:38;
hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A3, Th12; :: thesis: verum