theorem :: XREAL_1:60

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