Wrote up a proof of the statement 'AC implies LEM', as described by Valery Isaev: https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d