Set Theory This is a formalization of some results in set theory using extensional equality, classical logic, and the axiom of choice. One of the initial main results will be the Continuum Hypothesis for closed sets as proved by Cantor.