To start off, I will be giving a proof of the Tychonoff theorem of topology, the theorem says that if are compact topological spaces indexed by , then with the product topology is compact.

The following proof has the main idea illustrated in the following simpler theorem (the Königs lemma):

Take a poset and assume that every point has finite rank, that is, if then the cardinality of chains in are bounded by a natural number, the least bound is called the rank, so the minimal elements have rank zero, those after them have rank 1, etc. If we assume that the poset has infinite elements but finitely many of a given rank , then there exists an infinite chain (with the rank of equal to ).

The proof is simple but clever, first choose to be minimal such that it has infinitely many elements above it, it exists as there are infinite elements in the poset but finitely many minimal elements; after that choose minimal above having infinitely many elements above it (exists by similar considerations), etc. (strictly speaking “ is above ” here should be defined as having a chain with the required rank property).

The Tychonoff theorem can now be proved using the same idea with the technical padding of the analogy of “compact space” to “finite set” and transfinite recursion, the sets of rank being the space .

In full suppose by contradiction that there is an open cover of which has no finite subcover (we may assume it to consist of elements of the usual basis). Well order by a cardinal , may assume w.l.o.g that . Define with a transfinite recursion process on points with , and such that is not covered by a finite subcover of . At stage we get a contradiction.

At stage a limit ordinal, no new element needs to be chosen, and the process goes through by the finiteness in the definition of the product topology (i.e. it has a basis of the form where is open and* is equal to* *for all but finitely many indexes*), said differently if is covered by a finite subcover then for a .

At sucesor stage we need to choose with the infiniteness property, for this assume by contradiction that no such element exists, choose for each point an open neighborhood such that is covered by an open subcover and apply the compacity of