let x, y be R_eal; :: thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not -infty < x - y or ( x <> -infty & y <> +infty ) )
assume that
A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) and
A2: -infty < x - y ; :: 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:7; :: thesis: verum

end;

suppose y = +infty ; :: thesis: contradiction

hence contradiction by A1, A2, SUPINF_2:6; :: thesis: verum

end;

end;