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

hereby :: thesis: ( |.x.| <= y implies ( - y <= x & x <= y ) )

assume that
A1: - y <= x and
A2: x <= y ; :: thesis: |.x.| <= y
- x <= - (- y) by A1, XREAL_1:24;
hence |.x.| <= y by A2, Def1; :: thesis: verum

end;

assume A3: |.x.| <= y ; :: thesis: ( - y <= x & x <= y )
then A4: 0 <= y by COMPLEX1:46;

per cases ( 0 < x or x < 0 or x = - 0 ) ;

suppose 0 < x ; :: thesis: ( - y <= x & x <= y )

hence ( - y <= x & x <= y ) by A3, A4, Def1; :: thesis: verum

end;

suppose A5: x < 0 ; :: thesis: ( - y <= x & x <= y )

then - x <= y by A3, Def1;
then - y <= - (- x) by XREAL_1:24;
hence ( - y <= x & x <= y ) by A5; :: thesis: verum

end;

suppose x = - 0 ; :: thesis: ( - y <= x & x <= y )

hence ( - y <= x & x <= y ) by A3; :: thesis: verum

end;

end;