theorem :: EXTREAL1:17

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