theorem :: REAL:2

for x, y being Real st x <= y & y is negative holds
x is negative