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