  In this short note we give an alternative proof of Glivenko's Theorem,
stating that a formula $\phi$ is provable in classical propositional logic if
and only if $\neg\neg\phi$ is provable in intuitionistic propositional logic.
We work in the natural deduction system by Gentzen, and the key lemma shows
that in any proof one needs only one application of reductio ad absurdum.
