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