I try to prove $L_{SO}=\mathrm{HOD}$, where $L_{SO}$ is second-order constructible universe which has similar definition with $L$ but it uses second-order definability rather than the first-order definability, and I found the answer in MO. Also, I found the referred article in the answer which is written by Myhill and Scott.

The proof of $L_{SO}=\mathrm{HOD}$ in the answer mentioned previoisly and the article uses axiom of choice. (To be precise, it uses trichotomy for cardinals and they use it to prove $\mathrm{HOD}\subset L_{SO}$). My question is: using the axiom of choice is essential to prove $\mathrm{HOD}\subset L_{SO}$? Thanks for any information or clarification.