theorem :: REAL:1

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