theorem :: REAL:7

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