This writeup uses the notation of Sierpinski's Theorem, and anyway is a proof of what's there, so why don't you read that first?

There's a very elegant proof of Sierpinski's theorem with non-standard analysis. A "standard" proof, such as the one below, is surprisingly difficult and nonobvious. Nonetheless it is almost entirely elementary, apart from a well-hidden use of the Axiom of Choice.

We prove the theorem (that the equation

a1/x1 + ... + ak/xk = b.
with positive real number parameters a1,...,ak,b has only finitely many solutions in natural numbers x1,...,xk) by induction on k.

For k=1:
The theorem is obviously true: a/x=b has, at most, 1 solution x=a/b.
Assuming the theorem for k, we show it for k+1:
Suppose, to the contrary, that there are infinitely many solutions.

If, for some j, the same value of xj appears in infinitely many solutions: WLOG j=k+1 (just swap ak+1 and aj...), and the value c=xk+1 appears infinitely many times. But then the equation in k variables

a1/x1 + ... + ak/xk = b' = b-ak+1/d
has infinitely many solutions, contradicting the induction hypothesis.

Thus, every value of every xj appears only finitely many times. But this implies (set theorists will note that a version of the Axiom of Choice is involved here) that there are solutions with arbitrarily large xj's.

So there must exist a solution x1,...,xk+1 with ∀j.xj>aj⋅(k+1)/b. But this too is impossible! aj/xj < b/(k+1), so the sum

b = a1/x1 + ... + ak+1/xk+1 < b.

Thus, if there are only finitely many solutions to any Sierpinski equation with k variables, there can be only finitely many solutions to any Sierpinski equation with k+1 variables. The theorem follows by induction.

It is interesting to compare this with the NSA proof. Non-standard analysis requires more "setup time", at least if setting out from the usual techniques. But its clear formulation of concepts of compactness simplifies the proof. Even the tricky induction required in the standard setting is made redundant with NSA.