let x, y be real number ; :: thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )
A1: ( |.x.| <= y implies ( - y <= x & x <= y ) )

proof

assume A2: |.x.| <= y ; :: thesis: ( - y <= x & x <= y )
A3: ( x < - 0 implies ( - y <= x & x <= y ) )

proof

assume A4: x < - 0 ; :: thesis: ( - y <= x & x <= y )
then - x <= y by A2, Lm23;
then - y <= - (- x) by XREAL_1:26;
hence ( - y <= x & x <= y ) by A4; :: thesis: verum

end;

0 <= y by A2, Th132;
hence ( - y <= x & x <= y ) by A2, A3, Th129; :: thesis: verum

end;

( - y <= x & x <= y implies |.x.| <= y )

proof

assume that
A5: - y <= x and
A6: x <= y ; :: thesis: |.x.| <= y
- x <= - (- y) by A5, XREAL_1:26;
then ( x < 0 implies |.x.| <= y ) by Lm23;
hence |.x.| <= y by A6, Th129; :: thesis: verum

end;

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