Lying-over theorem without Axiom of Choice This question is motivated by this and this.
Can the following proposition be proved without Axiom of Choice?
Proposition:
Let $k$ be a field.
Let $A$ and $B$ be commutative algebras without zero-divisors which are finitely generated over $k$. Suppose that $A$ is a subring of $B$ and $B$ is integral over $A$.
Let $P$ be a prime ideal of $A$.
Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.
 A: First we show 

 Lemma If $A\to B$ is a finite homomorphism of rings with $A$ local and $B\ne 0$, then the maximal ideal $P$ of $A$ is the pre-image of a maximal ideal $Q$ of $B$. 

Proof. By Nakayama's lemma, $PB\ne B$. The quotient $B/PB$ is a finite $k$-algebra (where $k$ is the field $A/P$) and is no zero. The set of proper ideals of $B/PB$ is non-empty and has an element of maximal $k$-vector space dimension. The latter is then a maximal ideal, hence equal to $Q/PB$ for some maximal ideal $Q$ of $B$ containing $P$. The pre-image $P'$ of $Q$ is maximal because $A/P'$ is contained in $B/Q$ and the later is finite over $A/P'$. So $P'=P$. 
Now we prove your proposition. As $B$ is a finitely generated $A$-algebra, $B$ integral over $A$ implies that $B$ is finite over $A$. Hence $A_P\to A_P\otimes_A B$ is finite with $A_P\otimes_A B\ne 0$. By the above lemma, $PA_P$ is the pre-image of a maximal ideal of $A_P\otimes_A B$. The existence of $Q$ as desired follows from standard arguments on localizations. 
This been said, I agree with the second part of Martin Brandenburg's comment.
A: Definition 1
Let $A$ be a commutative ring.
Suppose $A$ has a unique maximal ideal.
We say $A$ is a local ring in the usual sense.
Definition 2
Let $A$ be a commutative ring.
Let $P$ be an ideal of $A$.
Suppose that every element of $A - P$ is invertible.
Then we say $A$ is a strictly local ring.
Clearly $P$ is the unique maximal ideal of $A$.
Hence $A$ is a local ring in the usual sense.
Note 1
It can be proved by using AC that a local ring in the usual sense is a strictly local ring.
However, we are not supposed to use AC here.
Lemma 1
Let $A$ be commutative ring.
Let $P$ be a prime ideal of $A$.
Then $A_P$ is a strictly local ring.
Proof:
Clear.
Definition 3
Let $A$ be a domain.
Let $P$ be a prime ideal of $A$.
Let $k$ be the field of fractions of $A/P$.
Let $K$ be a field which contains $A$ as a subring.
Let $x$ be an element of $K$.
Let $x'$ be an element of some field containing $k$.
We say $x'$ is a specialzation of $x$ over $P$ and we write $x \rightarrow x'$ over $P$,
if there exists a homomorophism $\psi:A[x] \rightarrow (A/P)[x']$ extending the canonical homomorphism $A \rightarrow A/P$ and $\psi(x) = x'$.
This is equivalent to that $\tilde{f}(x') = 0$ whenever $f(X) \in A[X]$ such that $f(x) = 0$,where $\tilde{f}(X) \in (A/P)[X]$ is the reduction of $f(X)$ mod $P$.
Lemma 2
Let $A$ be a strictly local domain.
Let $\mathfrak{m}$ be the unique maximal ideal of $A$.
Let $k = A/\mathfrak{m}$.
Let $K$ be a field which contains A.
Let $x \in K$.
Suppose $x$ has no specializaion in any finite extension field of $k$ over $\mathfrak{m}$.
Then $x$ is non-zero and $1/x \rightarrow 0$ over $\mathfrak{m}$.
Proof:
Let $P$ = {$f \in A[X]$; $f(x) = 0$}.
$P$ is an ideal of $A[X]$.
Let $P'$ be the ideal of $k[X]$ generated by the set {$f(X)$ (mod $\mathfrak{m}$); $f(X) \in P$}.
We claim that $P' = k[X]$.
Suppose otherwise.
Then $P'$ is generated by a polynomial $h(X) \in k[X]$, where $h(X)$ is not a non-zero constant.
Hence $h(X)$ has a root $x'$ in a finite extension of k.
Then $x \rightarrow x'$ over $\frak{m}$
This is a contradiction.
Hence there exists $f(X) \in P$ such that $f(X)$ (mod $\mathfrak{m}$) is a non-zero constant.
Let $f(X) = a_mX^m + ... + a_0$.
Then $a_0 \in A - \mathfrak{m}$, $a_i \in \mathfrak{m}$ for $i > 0$.
We assume that $m$ is minimal among the degrees of such polynomials.
Let $y = 1/x$.
Let $g(Y) = a_0Y^m + ... + a_m$ be a polynomial in $A[Y]$.
Then $g(y) = 0$.
Let $h(Y)$ be any polynomial in $A[Y]$ such that $h(y) = 0$.
Since $A$ is a strict local ring, $a_0$ is invertible.
Hence $Z^{m-1}h(Y) = g(Y)q(Y) + r(Y)$, where $q(Y), r(Y) \in A[Y]$ and deg $r \leq m - 1$.
Substituting $Y$ by $y$ we get $r(y) = 0$.
Taking the reductions mod $\mathfrak{m}$ of the both sides, we get
$Y^{m-1}\tilde{h}(Y) = \tilde{a_0}Y^m\tilde{q}(Y) + \tilde{r}(Y)$.
Hence $\tilde{h}(0) = \tilde{r}(Y)$.
Since $\tilde{r}(Y)$ cannot be a non-zero constant by the minimality of $m$, $\tilde{h}(0) = 0$.
Hence $z \rightarrow 0$ over $\mathfrak{m}$.
QED
Note 2
The idea of the proof of Lemma 2 is borrowed from Weil's Foundations of algebraic geometry. According to him, the idea is due to Chevalley.
See also Note 3 below.
Lemma 3
Let $A$ be a domain.
Let $P$ be a prime ideal of $A$.
Let $k$ be the field of fractions of $A/P$.
There exists a unique homomorphism $A_P \rightarrow k$ extending the canonical homomorphism $A \rightarrow A/P$.
Proof:
Clear.
Lemma 4
Let $A$ be a domain.
Let $P$ be a prime ideal of $A$.
Let $k$ be the field of fractions of $A/P$.
Let $K$ be a field which contains A as a subring.
Let $x \in K$.
Suppose $x$ has no specializaion in any finite extension of $k$ over $P$.
Then $x$ is non-zero and $1/x \rightarrow 0$ over $P$.
Proof:
Let $B = A_P$.
By lemma 1, $B$ is a strictly local ring.
Suppose $x \rightarrow x'$ over $PA_P$.
By Lemma 3, $x \rightarrow x'$ over $P$.
Hence $x$ has no specializaion in any finite extension of $k$ over $PA_P$.
By Lemma 2, $1/x \rightarrow 0$ over $PA_P$.
Hence, by Lemma 3, $1/x \rightarrow 0$ over $P$.
QED
Note 3
Lemma 4 is a generalization of the one given in Weil's Foundations. He proved it when $A$ is a finitely generated domain over a field.
Our Lemma 4 treats not only a case where $A$ and $A/P$ have equal characteristics but also a case of unequal ones.
Note 4
As van der Waerden and Weil showed, Lemma 4 has vast applications in algebraic geometry.
For example, Hilbert Nullstellensatz can be proved by using it.
Lemma 5
Let $A$ be a domain.
Let $P$ be a prime ideal of $A$.
Let $k$ be the field of fractions of $A/P$.
Let $K$ be a field which contains $A$ as a subring.
Let $x \in K$.
Suppose $x$ is integral over $A$.
Then there exist a finite extension $k'$ of $k$ and $x' \in k'$ such that $x \rightarrow x'$ over $P$.
Proof:
Suppose there exists no such x'.
By Lemma 4, there exists a homomorophism $\psi:A[1/x] \rightarrow k$ such that $\psi(1/x) = 0$ extending the canonical homomorphism $A \rightarrow A/P$.
Let $y = 1/x$.
Since $x$ is integral over $A$,
$x^n + a_1x^{n-1} + ... + a_0 = 0$.
Hence $1 + a_1y + ... + a_0y^n = 0$.
Applying $\psi$, we get $1 = 0$.
A contradiction.
QED
Proposition
Let $B$ be a domain.
Let $A$ be a subring of $B$.
Suppose $B$ is finitely generated as an $A$-module.
Let $P$ be a prime ideal of $A$.
Let $k$ be the field of fractions of $A/P$.
Then there exist a finite extension $k'$ of $k$ and a homomorophism $\psi:B \rightarrow k'$ extending the canonical homomorphism $A \rightarrow A/P$.
Proof:
This follows Immediately from Lemma 5.
Corollary
Let $B$ be a domain.
Let $A$ be a subring of $B$.
Suppose $B$ is finitely generated as an $A$-module.
Let $P$ be a prime ideal of $A$.
Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.
Proof:
This follows Immediately from the proposition.
