let x, y be ExtReal; :: thesis: ( not x + y = +infty or x = +infty or y = +infty )
assume A1: x + y = +infty ; :: thesis: ( x = +infty or y = +infty )
assume ( not x = +infty & not y = +infty ) ; :: thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = -infty ) ) by XXREAL_0:14;
hence contradiction by A1, Def2; :: thesis: verum