for x being ExtReal st |.x.| = - x & x <> 0 holds
x < 0