*The comments by The User and Joel David Hamkins refer to a previous version of the answer which contained a mistake. The current version is completely disjoint of the previous one, and the comments no longer apply.*

This appears in Tarski's book **Cardinal Algebras** as Theorem 2.28, called *Interpolation Theorem*, and the statement of the theorem is as follows:

If $n\leqq\infty,\ p\leqq\infty$, such that $a_i\leqq b_j$ for $i< n$ and $j < p$, then there is an element $c$ such that $a_i\leqq c\leqq b_j$ for every $i < n$ and $j < p$.

The theorem appears on page 27. The full citation is given below, one can also read about it on MathSciNet.

Tarski, Alfred. **Cardinal Algebras. With an Appendix: Cardinal Products of Isomorphism Types, by Bjarni Jónsson and Alfred Tarski.** *Oxford University Press,* New York, N. Y., 1949. xii+326 pp.

One note about the use of $\infty$ here, Tarski assumes that there is an operator of summation of a countable sequence, and therefore the theorem holds in that case as well. This may require the axiom of choice (or rather a minor fragment thereof), but if we remove that case, then the proof goes through just fine.

The proof begins with the case of $n=p=2$, in which cardinals are manipulated by hand. It then proceeds to the case where $n$ is arbitrary and $p=2$, where a sequence is defined by induction and the existence of a supremum is guaranteed by a previous theorem. Here we use choice when $n=\infty$, but if $n$ is finite then the induction halts and the upper bound of the last step is our wanted $x$.

Next he proves for $n=2$ and $p$ arbitrary. For finite $p$ the proof is purely constructive, and I suspect it holds without the axiom of choice for $p=\infty$ as well (it relies on previous theorems which I haven't read thoroughly in search of choices).

Lastly he argues that the proof of the general case follows as the proof of the second case, with using the third case to reason instead of the first case. In either case, if we assume $p,n<\infty$ then there is no invocation of the axiom of choice.