theorem Th3: :: POLYNOM5:3

for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0