let x be ExtReal; :: thesis: ( |.x.| = - x & x <> 0 implies x < 0 )
reconsider x = x as R_eal by XXREAL_0:def 1;
0 <= |.x.| ;
hence ( |.x.| = - x & x <> 0 implies x < 0 ) ; :: thesis: verum