theorem :: ABSVALUE:5

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