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

per cases ( x < 0 or 0 <= x ) ;

suppose A1: x < 0 ; :: thesis: ( - |.x.| <= x & x <= |.x.| )

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

end;

suppose A2: 0 <= x ; :: thesis: ( - |.x.| <= x & x <= |.x.| )

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

end;

end;