theorem Th9: :: EXTREAL1:20

for x being ExtReal holds
( - |.x.| <= x & x <= |.x.| )