and $w$ is true. Atoms $u$ and $w$ can be inferred for instance by some rule in (\[eq:red:fourth\]) whenever truth values of atoms of $P_\Phi$ represent a satisfying assignment for $\phi$. Furthermore, rules in (\[eq:red:fifth\]) are such that every model of $P_\Phi$ contains $v$, and any answer set of $P_\Phi$ must also contain $w$. We finally observe that $w$ can be derived by some rule in (\[eq:red:fourth\]) in the program reduct, which is the case if truth values of atoms in $X \cup \overline{X} \cup Y \cup \overline{Y}$ represent a consistent assignment for propositional variables in $X \cup Y$ satisfying $\forall Z \phi$.

Obviously, the program from above definition can be constructed in polynomial time in the size of the reduced QBF. To conclude the proof of Theorem \[thm:disj\] it is thus sufficient to show the following relation.

For any QBF $\Phi = \forall X\exists Y\forall Z\phi$, the program $P_\Phi$ is a $\Phi$-reduction.

Obviously, ${{\mathit At}}(P_\Phi)$ contains the atoms as required in 1) of Definition \[def:red\]. We continue to show 2). To see that $U$ is a model of $P_\Phi$ is obvious. We next show that the remaining models $M$ are all of the form $M[I,J]$ or $M'[I,J]$. First we 