Choice and well-ordering (Q579255)

It is proved that a well-ordering of a set S is intuitionistically definable from any choice function for S, finding an element in any non- void subset of S. The proof is presented in topos-theoretic setting. Main leading ideas are Diaconescu's theorem that the axiom of choice implies excluded middle and the classical derivation of well-ordering from choice. The author's guess was that the language of topos theory is necessary to present his proof, since its recasting in the language of intuitionistic set theory needs machines not yet in existence. Meanwhile such recasting was done by \textit{P. Aczel} [Every choice set can be well- ordered: An elementary proof in intuitionistic set theory, 14 typed pages] and the reviewer was told that A. Blass published a similar proof.