Existence of valuation rings in a finite extension of the field of fractions of a weakly Artinian domain without Axiom of Choice Can we prove the following theorem without Axiom of Choice?
This is a generalization of this problem. 
Theorem
Let $A$ be a weakly Artinian domain.
Let $K$ be the field of fractions of $A$.
Let $L$ be a finite extension field of $K$.
Let $B$ be a subring of $L$ containing $A$.
Let $P$ be a prime ideal of $B$.
Then there exists a valuation ring of $L$ dominating $B_P$.
As for why I think this question is interesting, please see(particularly Pete Clark's answer):
Why worry about the axiom of choice?
 A: Lemma 1
Let $A$ be an integrally closed weakly Artinian domain.
Let $S$ be a multiplicative subset of $A$.
Let $A_S$ be the localization with respect to $S$.
Then $A_S$ is an integrally closed weakly Artinian domain.
Proof:
Let $K$ be the field of fractions of $A$.
Suppose that $x \in K$ is integral over $A_S$.
$x^n + a_{n-1}x^{n-1} + ... + a_1x + a_0 = 0$, where $a_i \in A_S$.
Hence there exists $s \in S$ such that $sx$ is integral over $A$.
Since $A$ is integrally closed, $sx \in A$.
Hence $x \in A_S$.
Hence $A_S$ is integrally closed.
Let $f$ be a non-zero element of $A_S$.
$f = a/s$, where $a \in A, s \in S$.
Then $fA_S = aA_S$.
By this, $aA$ is a product of prime ideals of $A$.
Let $P$ be a non-zero prime ideal $P$ of $A$.
Since $P$ is maximal, $A_S/P^nA_S$ is isomorphic to $A/P^n$ or $0$.
Hence $leng_{A_S} A_S/aA_S$ is finite.
QED
Lemma 2
Let $A$ be an integrally closed weakly Artinian domain.
Let $P$ be a non-zero prime ideal of $A$.
Then $A_P$ is a discrete valuation ring.
Proof:
By Lemma 1 and this, every non-zero ideal of $A_P$ has a unique factorization as a product of prime ideals.
Hence $PA_P \neq P^2A_p$.
Let $x \in PA_P - P^2A_P$.
Since $PA_P$ is the only non-zero prime ideal of $A_P$, $xA = PA_P$.
Since every non-zero ideal of $A_P$ can be written $P^nA_P$, $A_P$ is a principal ideal domain.
Hence $A_P$ is a discrete valuation ring.
QED
Proof of the title theorem
We can assume that $P \neq 0$.
Let $C$ be the integral closure of $B$ in $L$.
By this, $C$ is a weakly Artinian $A$-algebra in the sense of Definition 2 of my answer to this.
By Lemma 2 of my answer to this, $C$ is a weakly Artinian ring.
Let $S = B - P$.
Let $C_P$ and $B_P$ be the localizations of $C$ and $B$ with respect to $S$ respectively.
By this, $leng_A C/PC$ is finite. Hence by Lemma 7 of my answer to this, $C/PC$ is finitely generated as an $A$-module.Hence $C/PC$ is finitely generated as a $B$-module.
Hence $C_P/PC_P$ is finitely generated as a $B_P$-module.
Since $PC_P \neq C_P$, by the lemma of the answer by QiL to this, there exists a maximal ideal of $C_P/PC_P$ whose preimage is $PB_P$.
Hence there exists a maximal ideal $Q$ of $C_P$ such tha $PB_P = Q \cap B_P$.
Let $Q' = Q \cap C$.
Then $Q'$ is a prime ideal of $C$ lying over $P$.
By Lemma 2, $C_Q'$ is a discrete valuation ring and it dominates $B_P$.
QED
