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][1]. 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. (Exactly, 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.


  [1]: http://mathoverflow.net/a/156949/48041