theorem Th5: :: FVALUAT1:5
for x, y being ExtReal st y <> +infty & x < 0 & 0 < y holds
x / y < 0