theorem :: ABSVALUE:20

for x, y being Real holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1