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|&lt;\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?
Perhaps a slighly shorter argument exploits saturation.  By countable saturation you can find an infinitesimal $\alpha&gt;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|&lt;\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$.
"Hyperfinitely many" in Robinsonian NSA translates to "finitely many" in IST, so you are asking whether there is a finite subset of an infinite set.