Does an internal set with countably many infinitesimals contain hyperfinitely many infinitesimals? Let $\mathscr{A}$ be an internal subset of $^*\mathbb{R}$ that contains a countable family, say $\{a_n\}_{n\in\mathbb{N}}$, of infinitesimal members, that is $a_n\approx 0$ for all $n\in\mathbb{N}$.
We can extend the sequence $a\colon\mathbb{N}\to\mathscr{A}$ to an internal hypersequence with the same name $a\colon{^*\mathbb{N}}\to\mathscr{A}$. It follows that the set
$$ \{n\in{^*\mathbb{N}}\mid |a_n|<\frac{1}{n}\} $$
is internal by the Internal Definition Principle and includes $\mathbb{N}$ by our assumption. Hence, by the Overflow Principle, there exists $H\in{^*\mathbb{N}}\setminus\mathbb{N}$ such that $a_N\approx 0$ for all $N\in{^*\mathbb{N}}$ with $N\leq H$.
Since the extended hypersequence $a$ is internal, $\{a_0,\dots,a_H\}$ is an infinite hyperfinite set of infinitesimal elements of $\mathscr{A}$.
Is this procedure correct? Is there a less sophisticated way to prove the statement? 
 A: Perhaps a slighly shorter argument exploits saturation.  By countable saturation you can find an infinitesimal $\alpha>0$ such that each of the countably many infinitesimals is smaller than $\alpha$ in absolute value.  Then the subset $\{x\in\mathcal{A}\colon |x|<\alpha\}$ is internal, infinite, and therefore is infinite hyperfinite.
The existence of such an upper bound $\alpha$ can be established as follows.  Suppose not; then wlog we can assume that the sequence $\langle\epsilon_n\colon n\in \mathbb N\rangle$ of positive infinitesimals is nondecreasing. Consider the hyperreal interval $S_n=[\epsilon_n,\frac{1}{n}]$. Then $\langle S_n\colon n\in\mathbb N\rangle$ is a nested sequence and by saturation it must have a common element $c$. But $c$ can be neither infinitesimal nor appreciable. The contradiction proves the existence of $\alpha$.
A: Translating the question into the language of Edward Nelson's internal set theory (IST) reduces it to triviality: "hyperfinitely many" in Robinsonian NSA translates to "finitely many" in IST, so the question asks whether there is a finite subset of an infinite set.
The answer is yes.
(Please read the discussion in the comments for further details.)
