let a be Real; :: thesis: [\a/] + [\(- a)/] is weightless

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

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

then - [\a/] = [\(- a)/] ;
hence [\a/] + [\(- a)/] is weightless ; :: thesis: verum

end;

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

hence [\a/] + [\(- a)/] is weightless ; :: thesis: verum

end;

end;