let x, y be R_eal; :: thesis: ( x <> +infty & x <> -infty & x * y = -infty & not y = +infty implies y = -infty )
assume A1: ( x <> +infty & x <> -infty & x * y = -infty ) ; :: thesis: ( y = +infty or y = -infty )
assume A2: ( y <> +infty & y <> -infty ) ; :: thesis: contradiction
reconsider a = x as Real by A1, XXREAL_0:14;
reconsider b = y as Real by A2, XXREAL_0:14;
x * y = a * b by Th13;
hence contradiction by A1; :: thesis: verum