let x, y be ExtReal; :: thesis: ( x <> +infty & x <> -infty & x * y = -infty & not y = +infty implies y = -infty )
assume that
A1: ( x <> +infty & x <> -infty ) and
A2: x * y = -infty ; :: thesis: ( y = +infty or y = -infty )
assume ( y <> +infty & y <> -infty ) ; :: thesis: contradiction
then A3: y in REAL by XXREAL_0:14;
x in REAL by A1, XXREAL_0:14;
then reconsider a = x, b = y as Real by A3;
x * y = a * b ;
hence contradiction by A2; :: thesis: verum