theorem Th102: :: XXREAL_3:102

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