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;