theorem Th12: :: EXTREAL1:23
for x, y being ExtReal holds
( ( - y <= x & x <= y ) iff |.x.| <= y )