let x, y be Real; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A1: ( ( x = 0 or y = 0 ) implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

A2: ( y = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

A3: (sgn x) - 1 < ((sgn x) + (- 1)) + 1 by XREAL_1:29;
assume A4: y = 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then ((sgn x) + (sgn y)) - 1 = ((sgn x) + 0) - 1 by Def2
.= (sgn x) - 1 ;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A4, A3; :: thesis: verum

end;

A5: ( x = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

A6: (sgn y) - 1 < ((sgn y) + (- 1)) + 1 by XREAL_1:29;
assume A7: x = 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then ((sgn x) + (sgn y)) - 1 = (0 + (sgn y)) - 1 by Def2
.= (sgn y) - 1 ;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A7, A6; :: thesis: verum

end;

assume ( x = 0 or y = 0 ) ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A5, A2; :: thesis: verum

end;

A8: ( x < 0 & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A9: x < 0 and
A10: y < 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
sgn x = - 1 by A9, Def2;
then A11: sgn x = sgn (x + y) by A9, A10, Def2;
A12: ( ((sgn (x + y)) + (- 1)) - 1 < (((sgn (x + y)) + (- 1)) - 1) + 1 & (sgn (x + y)) + (- 1) < ((sgn (x + y)) + (- 1)) + 1 ) by XREAL_1:29;
sgn y = - 1 by A10, Def2;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A11, A12, XXREAL_0:2; :: thesis: verum

end;

A13: ( 0 < x & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A14: 0 < x and
A15: y < 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
sgn x = 1 by A14, Def2;
then A16: (sgn x) + (sgn y) = 1 + (- 1) by A15, Def2
.= 0 ;
( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A16, Def2; :: thesis: verum

end;

A17: ( x < 0 & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A18: x < 0 and
A19: 0 < y ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
sgn x = - 1 by A18, Def2;
then A20: (sgn x) + (sgn y) = (- 1) + 1 by A19, Def2
.= 0 ;
( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A20, Def2; :: thesis: verum

end;

( 0 < x & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A21: 0 < x and
A22: 0 < y ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
sgn y = 1 by A22, Def2;
then ((sgn x) + (sgn y)) - 1 = 1 by A21, Def2;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A21, A22, Def2; :: thesis: verum

end;

hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A8, A17, A13, A1; :: thesis: verum