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

proof

assume A2: x < 0 ; :: thesis: ( - |.x.| <= x & x <= |.x.| )
then |.x.| = - x by Lm23;
hence ( - |.x.| <= x & x <= |.x.| ) by A2; :: thesis: verum

end;

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

proof

assume A3: 0 <= x ; :: thesis: ( - |.x.| <= x & x <= |.x.| )
then - x <= - 0 ;
hence ( - |.x.| <= x & x <= |.x.| ) by A3, Th129; :: thesis: verum

end;

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