let x, y be ExtReal; :: thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )

A1: ( - y <= x & x <= y implies |.x.| <= y ) ( |.x.| <= y implies ( - y <= x & x <= y ) ) hence ( ( - y <= x & x <= y ) iff |.x.| <= y ) by A1; :: thesis: verum

A1: ( - y <= x & x <= y implies |.x.| <= y ) ( |.x.| <= y implies ( - y <= x & x <= y ) ) hence ( ( - y <= x & x <= y ) iff |.x.| <= y ) by A1; :: thesis: verum