Choose from every nonempty subset of . By transfinite recursion set
while the remainder is nonempty. This cannot continue through Hartogs theorem's ordinal , since that would inject into . It therefore exhausts at some ordinal, and the selection order well-orders .
Choice well-orders every infinite , so Hessenberg gives . Conversely assume this square identity for every infinite set. For arbitrary , form the disjoint union . A pairing , together with the well-order on , yields by the standard tracing/comparison argument an injection either or . The first is forbidden by Hartogs theorem, so the second well-orders . This is Tarski cardinal-square theorem, and hence choice follows.
Assume the axiom of choice and suppose a poset satisfying the hypothesis has no maximal element. Fix a choice function on its nonempty subsets. By transfinite recursion, choose at each ordinal stage an upper bound of the chain in a partial order already constructed, then choose a strictly larger member. Both choices are available, including the initial empty stage. This produces distinct members throughout the Hartogs ordinal of , contradicting the Hartogs theorem. Thus a maximal element exists. Conversely, apply Zorn's lemma to partial choice functions on a family of nonempty sets, ordered by extension. A chain in a partial order has the compatible union as an upper bound, and a maximal element must be defined on the whole family, since one missing value could be adjoined.
Zorn's lemma was introduced in 1935 to shorten algebra proofs using choice or the well-ordering theorem.[ref]