This question is motivated by the discussion in the comments to [this
post](https://mathoverflow.net/q/454016/28128).  The question concerns
a comparison of model-theoretic (extension) approaches to nonstandard
analysis, and axiomatic (syntactic) approaches such as
[IST](https://en.wikipedia.org/wiki/Internal_set_theory), BST, HST,
and others.

Consider the following two examples.

1. An internal subset of $\mathbb R^\ast$ which is already contained
in $\mathbb R\subseteq \mathbb R^\ast$ is necessarily finite.  The
proof of this as found in a popular textbook such as
[Goldblatt's](https://scholar.google.com/scholar?cites=4118501315415182310)
is somewhat involved.  Meanwhile, in axiomatic set theories, the fact
that an infinite set must contain nonstandard elements is immediate
from Idealisation.

2. Overspill: every internal subset of $\mathbb N^\ast$ containing
$\mathbb N$ must also contain a nonstandard integer, or equivalently an internal
set containing all nonstandard integers must contain a standard
integer.  Proofs in the model-theoretic approach need to develop
*internal induction* or *internal well-ordering* first, whereas in the
axiomatic approach one just applies the usual well-ordering property of $\mathbb N$ to
derive a contradiction from the existence of a set of all nonstandard
integers.

I am looking for further examples of this type so as to illustrate the
fact that sometimes axiomatic approaches have their advantages
over the model-theoretic ones (and vice versa).  The kind of examples
I am looking for would preferably be applicable also to the weaker
systems SPOT or SCOT.  Note that, even though the axioms of SPOT do
not include idealisation, one can actually prove countable
Idealisation within SPOT.