theorem Th9: :: FVALUAT1:9

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