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

then A4: 0 <= y by COMPLEX1:46;

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

assume A3:
|.x.| <= y
; :: thesis: ( - 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;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

then A4: 0 <= y by COMPLEX1:46;