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