let a be non integer Real; :: thesis: [\a/] + [\(- a)/] = - 1
sgn (frac a) = 1 by COMPLEX3:1;
then ([\a/] + [\(- a)/]) + 1 = 0 by FL;
hence [\a/] + [\(- a)/] = - 1 ; :: thesis: verum