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