I'll just remark that the fact that every surface has a finite number of excluded minors (and also topological minors) does not require the full strength of the Graph Minors Theorem.  Indeed, the proof relies on the following three facts:

1. **The Grid Theorem**.  There exists a function $f: \mathbb{N} \to \mathbb{N}$, such that every graph with tree-width at least $f(n)$, contains the $n \times n$ grid as a minor.

2. **Graphs of bounded tree-width are well-quasi-ordered.**  For any $k$, the class of graphs of tree-width at most $k$ is well-quasi-ordered.

3. **Forbidden minors for surfaces do not contain arbitrarily large grid minors.**  There is a function $h: \mathbb{N} \to \mathbb{N}$, such that every minor-minimal graph not embeddable on a surface of genus $g$ does not contain an $h(g) \times h(g)$ grid as a minor.  

All three of these facts now have very compact proofs.  In fact, proofs for (1) and (3), and a sketch of a proof of (2) can be found in Diestel's *Graph Theory* textbook.  See [here](http://diestel-graph-theory.com/) to peruse the book online.