theorem :: REAL:3

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