i dont understand why axiom of choice is needed for the proof, since X is finite and (if i haven't misunderstand anything) we don't need axiom of choice to define a choice function for a finite set.
The proof: https://proofwiki.org/wiki/Axiom_of_Choice_Implies_Law_of_Excluded_Middle