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