let x be ExtReal; :: thesis: ( x <= 0 implies |.x.| = - x )
assume A1: x <= 0 ; :: thesis: |.x.| = - x

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

suppose x < 0 ; :: thesis: |.x.| = - x

hence |.x.| = - x by Def1; :: thesis: verum

end;

suppose A2: x = 0 ; :: thesis: |.x.| = - x

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

end;

end;