Corollary 12.3
(Chevalley’s Theorem)
.
Assuming that:
K
⊨
ACF
X
⊆
K
n
a constructible set
Then
the projection
Y
=
{
(
a
1
,
…
,
a
n
−
1
)
∈
K
n
−
1
:
(
a
¯
,
b
)
∈
X
for some
b
∈
K
}
of
X
is also constructible.