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:6; :: thesis: verum

end;

suppose y = -infty ; :: thesis: contradiction

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

end;

end;