theorem :: ABSVALUE:4

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