theorem Th20: :: XXREAL_3:20

for x, y being ExtReal holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )