theorem Th5: :: CARDFIL4:5

for r being Real st 0 < r holds
ex m being Nat st
( not m is zero & 1 / m < r )