theorem Th72: :: XXREAL_3:72

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