theorem Th71: :: XXREAL_3:71

for x, y, z being ExtReal st x <= y & 0 <= z holds
x * z <= y * z