This question is motivated by the discussion in the comments to this post. The question concerns a comparison of model-theoretic (extension) approaches to nonstandard analysis, and axiomatic (syntactic) approaches such as IST, BST, HST, and others.
Consider the following two examples.
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 is somewhat involved. Meanwhile, in axiomatic set theories, the fact that an infinite set must contain nonstandard elements is immediate from Idealisation.
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.