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

suppose A1: 0 <= x ; :: thesis: not |.x.| is negative

then |.x.| = x by Def1;
hence not |.x.| is negative by A1; :: thesis: verum

end;

suppose A2: x < 0 ; :: thesis: not |.x.| is negative

then |.x.| = - x by Def1;
hence not |.x.| is negative by A2; :: thesis: verum

end;

end;