It is a well known fact that Zermelo's Axiom of Choice and Zorn's Lemma are equivalent logical assumptions. However, an investigation from the viewpoint of the hierarchy of types reveals a complication in the nature of this equivalence. In a type-theoretical formalism both postulates enter as spectra (ZAα) and (ZLα) of formulas, where ZAα is Zermelo's Axiom and ZLα is Zorn's Lemma stated for variables of a fixed type α. The complication has its origin in the fact that, although the formula ZAα implies ZLα, in order to deduce ZAα it seems to be necessary to assert Zorn's Lemma ZLβ for a type β which is higher than α. In other words, we don't know a proof assuring the equivalence of the two formulas ZAα and ZLα. Therefore the equivalence of Zermelo's Axiom and Zorn's Lemma has to be understood in the sense that the assertion of the formulas ZAα for all types α implies every one of the formulas ZLβ and conversely the assertion of the spectrum of formulas (ZLα) implies every one of the formulas ZAβ.

In § 3 we shall indicate a type β which makes the deduction of ZAα from ZLβ possible. For this purpose a proof by G. Birkhoff [3] is translated into type-theoretical language.

In § 2 it is shown that ZAα implies ZLα. In this proof no use is made of the notion of well-ordering. Specifically, we do not first deduce the Well-Ordering Theorem as it is usually done in proving Zorn's Lemma from Zermelo's Axiom. However, the method is suggested by Zermelo's second proof of the Well-Ordering Theorem [2].