theorem PP: :: FINANCE5:2

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