theorem :: REAL:6

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