theorem :: REAL:4

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