let a be Real; :: thesis: ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0

per cases ( a is integer or not a is integer ) ;

suppose a is integer ; :: thesis: ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0

then reconsider a = a as Integer ;
( [\a/] = a & [\(- a)/] = - a & sgn (frac a) = 0 ) ;
hence ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0 ; :: thesis: verum

end;

suppose not a is integer ; :: thesis: ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0

then reconsider a = a as non integer Real ;
( [\a/] < a & [\(- a)/] < - a ) by INT_1:26;
then [\a/] + [\(- a)/] < a + (- a) by XREAL_1:8;
then A1: [\a/] + [\(- a)/] <= - 1 by INT_1:8;
( a - 1 < [\a/] & (- a) - 1 < [\(- a)/] ) by INT_1:def 6;
then (a - 1) + ((- a) - 1) < [\a/] + [\(- a)/] by XREAL_1:8;
then (- 2) + 1 <= [\a/] + [\(- a)/] by INT_1:7;
then [\a/] + [\(- a)/] = - 1 by A1, XXREAL_0:1
.= - (sgn (frac a)) by COMPLEX3:1 ;
then ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0 ;
hence ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0 ; :: thesis: verum

end;

end;