Description: Zorn's Lemma of Monk1 p. 117. This theorem is equivalent to the Axiom
of Choice and states that every partially ordered set A (with an
ordering relation R ) in which every totally ordered subset has an
upper bound, contains at least one maximal element. The main proof
consists of lemmas zorn2lem1 through zorn2lem7 ; this final piece
mainly changes bound variables to eliminate the hypotheses of
zorn2lem7 . (Contributed by NM, 6-Apr-1997)(Revised by Mario
Carneiro, 9-May-2015)