theorem :: REAL:5

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