theorem Th101: :: XXREAL_3:101

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