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