theorem Th86: :: XXREAL_3:86

for y being ExtReal st 0 < y & y <> +infty holds
-infty / y = -infty