theorem :: ABSVALUE:15

for x being Real st sgn x = - 1 holds
x < 0