A way to proof that any two Rado graphs (countably infinite nodes, has graph extension property) are isomorphic, is to use the back and forth method.
At each step of the method, we have a vertex $v$ in one graph. Using the graph extension property, we find (possibly countable infinite) vertices to map $v$ to.
Since we have to choose one of those vertices, why doesn't this use the axiom of choice?
From a quick look at the proof you link, at the beginning, we fixed an enumeration of each graph. Then at each step, we choose the lowest-numbered vertex that does what we want. We are making a specific choice, not an arbitrary one, so the axiom of choice is not needed.