theorem :: ABSVALUE:23

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