for x, y, z being ExtReal st x <= y & z < 0 holds
y / z <= x / z by Th101;