let a be Real; :: thesis: ( - |.a.| <= a & a <= |.a.| )
( a < 0 implies ( - |.a.| <= a & a <= |.a.| ) )

proof

assume a < 0 ; :: thesis: ( - |.a.| <= a & a <= |.a.| )
then |.a.| = - a by Lm27;
hence ( - |.a.| <= a & a <= |.a.| ) ; :: thesis: verum

end;

hence ( - |.a.| <= a & a <= |.a.| ) by Th43; :: thesis: verum