Let $\mathcal{O}$ be the set of strict total orders on $\kappa$. Each is a subset of $\kappa \times \kappa$, so the square of an infinite cardinal givesFor the lower bound, use the set $\kappa \times \{0,1\}$ and order the two-element blocks by their first coordinates, using the well-order of $\kappa$. For every $A\subseteq \kappa$, put $(\alpha ,0)$ before $(\alpha ,1)$ exactly when $\alpha \in A$, reversing them otherwise. This defines a strict total order for each $A$, and different subsets give different orders. Transport these orders to $\kappa$ along a fixed bijection $\kappa \times \{0,1\}\cong \kappa$. Thus $2^{\kappa }\le |\mathcal{O}|$, and the Cantor-Schröder-Bernstein theorem givesIf using the customary axiom of choice development of infinite cardinal arithmetic, its use here is precisely to supply $\kappa \times \kappa \cong \kappa$ and $\kappa \times 2\cong \kappa$. The ordering construction makes no further choices. It proves the cardinality of the family of strict total orders. For $\kappa$ itself an initial ordinal, these particular product identities can also be proved in ZF by well-ordering pairs according to their maximum coordinate, so full axiom of choice is stronger than this instance intrinsically requires.

For the standard definition of algebraic independence, finite tuples are required to have distinct entries. Let $\mathcal{P}$ be the set of all subsets of $L$ with algebraic independence over $K$, ordered by inclusion. It is nonempty because $\varnothing \in \mathcal{P}$.

If $\mathcal{C}$ is a chain in $\mathcal{P}$, put $U=\bigcup \mathcal{C}$. A finite tuple of distinct elements of $U$ lies in one member of $\mathcal{C}$: choose a member containing each element and take the largest of those finitely many members. A polynomial relation on that tuple would then be a polynomial relation in that member, contradicting its algebraic independence. Thus $U\in \mathcal{P}$ and is an upper bound. For the empty chain, $\varnothing$ is an upper bound. The Zorn's lemma now gives a maximal member $B$, which is a transcendence basis by the specified maximality criterion. To also recover the usual field-theoretic definition, if $a\in L$ were transcendental over $K(B)$, clearing denominators in a polynomial relation would show that $B\cup \{a\}$ still has algebraic independence over $K$, contradicting maximality. Thus $L$ is algebraic over $K(B)$. Hence every field extension has a transcendence basis.

There is a literal issue in the printed definition: it does not require the tuple entries to be distinct. With that wording, any nonempty $X$ fails the test: for $a\in X$, the nonzero polynomial $X_1-X_2$ vanishes on $(a,a)$, in every characteristic. Thus under the literal printed test the family is exactly $\{\varnothing \}$, and $\varnothing$ is its maximal member. The same chain-and-Zorn's lemma argument still proves existence for that literal notion, but it is not the usual transcendence basis notion. The conventional result above uses distinct tuple entries.

Assume the well-ordering theorem. Every set with a chosen well-order has an order isomorphism to a unique ordinal. Any two ordinals are comparable, and the smaller embeds into the larger as an initial segment. Transporting that embedding back to the original sets proves the cardinal comparability principle.

Conversely, assume the cardinal comparability principle and let $X$ be any set. The Hartogs theorem, provable in ZF, supplies an ordinal $h(X)$ for which no injection $h(X)\hookrightarrow X$ exists. Comparison forces an injection $X\hookrightarrow h(X)$. Pulling back the well-order on its image gives a well-order on $X$. ThereforeThe assumed ordinal facts are that every well-ordered set has an ordinal order type and that any two ordinals are comparable; the other assumed theorem is precisely the stated Hartogs theorem.

The four principles are:

In the last assertion the upper bound belongs to the partially ordered set; it need not belong to the chain.

The Cantor-Schröder-Bernstein theorem states that injections $A\hookrightarrow B$ and $B\hookrightarrow A$ imply a bijection $A\cong B$.

Let $\mathfrak{c}=|\mathbb{R}|$ and $\mathcal{D}=\{S\subseteq \mathbb{R}:S\text{ is dense in }\mathbb{R}\}$. Clearly $|\mathcal{D}|\le 2^{\mathfrak{c}}$. For the reverse bound, let $C$ be the usual Cantor set, of cardinality $\mathfrak{c}$. It is closed with empty interior, so $D=\mathbb{R}\setminus C$ is dense. The mapis injective, because $A=(D\cup A)\cap C$. Applying the Cantor-Schröder-Bernstein theorem givesOne can see $|C|=\mathfrak{c}$ by coding binary sequences as ternary expansions using only digits zero and two, together with the usual $|\{0,1{\}}^{\omega }|=|\mathbb{R}|$. The same fixed $D$ works for all subsets. This is the cardinality of the family of dense subsets of the reals.

A logical derivation is a finite proof in the specified calculus, with conclusion $\Gamma ⊢\varphi$. Assumptions from $\Gamma$ and instances of A1–A7 are available; the rules are the modus ponens rule, universal generalization rule, and weakening.

In judgement form the universal generalization rule takes $\Delta ⊢\theta$ to $\Delta ⊢\forall x_i\theta$ only if $x_i$ is not free in any undischarged assumption in $\Delta$. Weakening permits $\Delta ⊢\theta$ to become $\Delta \cup \Sigma ⊢\theta$. All instances of A4 and A5 must meet their stated substitution and free variable conditions. Derivability means existence of such a finite proof with assumptions contained in $\Gamma$. Equivalently one tracks the finite assumption set used by each proof line.