A variation of the axiom of choice

I found an unfamiliar form of AC in the proof of Zorn's lemma in ZFC by Lewin (1991). I don't even know whether it is natural or not.

$ (X, \le) $ is a poset. In the 5th paragraph of the paper, he introduced ($\exists$ elimination) a choice function $f$ from the family of chains of $X$ to $X$ such that for every chain $C$, $ f(C) $ is a strict upper bound of $C$.

But it seems that is not a direct application of AC in a usual form as presented in Wikipedia because $f(C) \notin C$ for every chain $C$.

How is it justified?

Comment: I called $f$ a choice function but it is not adequate because $f$ is the composition of an index function and a choice function according to Karagila The value of the index function is always nonempty exists because we assumed that $X$ has no maximal member.

Solution 1:

This is quite a natural way of thinking about the axiom of choice. If $C$ is a chain, let $U(C)$ denote the strict upper bounds of $C$. Then the choice function is from $\{U(C)\mid C\subseteq X\text{ is a chain}\}$.

By composing the indexing function, mapping $C$ to $U(C)$ with the chain function, we can think of this as a function assigning each chain a strict upper bound.