theorem Th70: :: XXREAL_3:70

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