Work in intuitionistic logic (IL), and assume ZF.
The Axiom of Choice (AC) implies both Zorn’s Lemma (ZL) and the law of excluded middle (EM). Furthermore, AC is the “join” of ZL and EM, since we can prove AC if we assume both of these principles.
The “meet” of ZL and EM is the set of formulas that are both provable from ZL (alone) and provable from EM (alone). What do we know about this meet? For example, is it equivalent to a single proposition in the language of set theory?