for x being Real st |.x.| = - x & x <> 0 holds
x < 0 by Def1;