theorem Th1: :: UNIFORM1:1
for r being Real st r > 0 holds
ex n being Nat st
( n > 0 & 1 / n < r )