let a be non integer Real; :: thesis: [\a/] + [\(- a)/] = - 1
A1: ( a = [\a/] + (frac a) & - a = [\(- a)/] + (frac (- a)) ) by INT_1:42;
(frac a) + (frac (- a)) = 1 by NEWTON06:10;
hence [\a/] + [\(- a)/] = - 1 by A1; :: thesis: verum