theorem :: XREAL_1:59

for a, b being Real st a <= - b holds
a + b <= 0