theorem :: XXREAL_3:16

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