let x, y be ext-real number ; :: 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 ( y <> +infty & y <> -infty ) ; :: thesis: contradiction
then ( x in REAL & y in REAL ) by A1, XXREAL_0:14;
then reconsider a = x, b = y as real number ;
x * y = a * b ;
hence contradiction by A1; :: thesis: verum