theorem Th20: :: EXTREAL1:31

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