let x, y be R_eal; :: thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < +infty or ( x <> +infty & y <> +infty ) )
assume that
A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) ) and
A2: x + y < +infty ; :: thesis: ( x <> +infty & y <> +infty )
assume A3: ( x = +infty or y = +infty ) ; :: thesis: contradiction

per cases ( x = +infty or y = +infty ) by A3;

suppose x = +infty ; :: thesis: contradiction

hence contradiction by A1, A2, SUPINF_2:def 2; :: thesis: verum

end;

suppose y = +infty ; :: thesis: contradiction

hence contradiction by A1, A2, SUPINF_2:def 2; :: thesis: verum

end;

end;