let x be R_eal; :: thesis: ( |.x.| = - x & x <> 0 implies x < 0 )
assume A1: ( |.x.| = - x & x <> 0 ) ; :: thesis: x < 0
assume A2: not x < 0 ; :: thesis: contradiction
then - x = x by A1, EXTREAL1:def 3;
hence contradiction by A1, A2, EXTREAL1:25; :: thesis: verum