Theorem 1.1.1 (Diaconescu). The law of excluded middle can be intuitionistically deduced from the Axiom of Choice.