theorem :: REAL:8

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