theorem Th85: :: XXREAL_3:85
for y being ExtReal st y < 0 & -infty <> y holds
+infty / y = -infty