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

proof

assume A2: |.a.| <= b ; :: thesis: ( - b <= a & a <= b )
( a < - 0 implies ( - b <= a & a <= b ) )

proof

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

end;

hence ( - b <= a & a <= b ) by A2, Th129; :: thesis: verum

end;

( - b <= a & a <= b implies |.a.| <= b )

proof

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

end;

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