theorem :: XXREAL_3:17

for x, y being ExtReal holds
( not x + y = -infty or x = -infty or y = -infty ) by Lm9;