let a be Real; :: thesis: [\a/] = - [/(- a)\]

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

suppose a is integer ; :: thesis: [\a/] = - [/(- a)\]

then ( [\a/] = a & - (- a) = - [/(- a)\] ) by INT_1:30;
hence [\a/] = - [/(- a)\] ; :: thesis: verum

end;

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

then reconsider a = a as non integer Real ;
[\a/] + [\(- a)/] = - 1 by FLM;
then ( [\a/] = - ([\(- a)/] + 1) & not [/(- a)\] = [\(- a)/] ) by INT_1:34;
hence [\a/] = - [/(- a)\] by INT_1:41; :: thesis: verum

end;

end;