State and formalize the main theorem.