for x, y being ExtReal st ( x is Real or y is Real ) holds
|.(|.x.| - |.y.|).| <= |.(x - y).|