theorem :: NUMERAL3:83

for a being Real holds [\a/] + [\(- a)/] is weightless