So, I can understand how [non-standard analysis](https://en.wikipedia.org/wiki/Non-standard_analysis) is better than standard analysis in that some proofs become simplified, and infinitesimals are somehow more intuitive to grasp than epsilon-delta arguments (both these points are debatable).


However, although many theorems have been proven by non-standard analysis and transferred via the [transfer principle](https://en.wikipedia.org/wiki/Transfer_principle), as far as I know all of these results were already known to be true. So, my question is:


Is there an example of a result that was *first* proved using non-standard analysis? To wit, is non-standard analysis actually useful for proving *new* theorems?


**Edit**: Due to overwhelming support of François' [comment](https://mathoverflow.net/questions/16312/how-helpful-is-non-standard-analysis#comment30082_16312), I've changed the title of the question accordingly.



How helpful is non-standard analysis?
From the [Wikipedia article](https://en.wikipedia.org/wiki/Non-standard_analysis#Applications):



> 
> the list of new applications in
> mathematics is still very small. One
> of these results is the [theorem proven
> by Abraham Robinson and Allen
> Bernstein](https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-16/issue-3/Solution-of-an-invariant-subspace-problem-of-K-T-Smith/pjm/1102994835.full) that every polynomially
> compact linear operator on a Hilbert
> space has an invariant subspace. Upon
> reading a preprint of the
> Bernstein-Robinson paper, [Paul Halmos
> reinterpreted their proof using
> standard techniques](https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-16/issue-3/Invariant-subspaces-of-polynomially-compact-operators/pjm/1102994836.full). Both papers
> appeared back-to-back in [the same
> issue of the Pacific Journal of
> Mathematics](https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-16/issue-3). Some of the ideas used in
> Halmos' proof reappeared many years
> later in Halmos' own work on
> quasi-triangular operators.
> 
> 
> 


