let x be real number ; :: thesis: ( - (abs x) <= x & x <= abs x )

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

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

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

end;

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

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

end;

end;