theorem Th3: :: FVALUAT1:3

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