theorem Th69: :: XXREAL_3:69

for x, y being ExtReal st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds
y = -infty