theorem Th9: :: EXTREAL1:20
for x being ExtReal holds
( - |.x.| <= x & x <= |.x.| )