$A = \q Y_C A'$, then $A$\*=$\q Y^{\ast} A'$\*. By the induction hypothesis, we have $\v_{LAF2} (A'[G/X_C])$\* $\equi A'$\*$[\neg G$\*$/X_C]$. Therefore $\v_{LAF2}
    (\q Y_C A'[G/X_C])$\*$ \equi$ $ (\q Y_C A')$\*$[\neg G$\*$/X_C]$. $\Box$

If $A_1,...,A_n \v_{LM2} A$, then $A_1$\*$,...,A_n$\* $\v_{LAF2} A$\*.

**Proof By induction on the proof of $A$ and using Lemmas 3.2, 3.3, and 3.4. $\Box$**

Let $A,A_1,...,A_n$ be formulas of $LAF2$.\
$A_1,...,A_n \v_{LM2} A$ if and only if $A_1,...,A_n \v_{LAF2} A$.

**Proof We use Theorem 3.2. $\Box$\
With each predicate variable $X$ of $C2$, we associate a classical variable $X_C$ having the same arity as $X$. For each formula $A$ of $LC2$, we define the formula $A^C$ of $M2$ in the following way :**

-   - If $A=D(t_1,...,t_n)$ where $D$ is a constant symbol, then $A^C=A$ ;

-   - If $A=X(t_1,...,t_n)$ where $X$ is a predicate symbol, then $A^C=X_C(t_1,...,t_n)$ ;

-   - If $A=B \f C$, then $A^C=B^C \f C^C$ ;

-   - If $A=\q xB$, then $A^C=\q xB^C$ ;

-   - If $A=\q XB$, then $A^C=\q X_CB^C$.

$A^C$ is called the classical translation of $A$.

Let $A_1,...,A_n,A$ be formulas of $LC2$.\
$A_1,...,A_n \v_{LC2} A$ if and only if $A_1^C,...,A_n^C \v_{LM2} A^C$.

**Proof By induction on the proof of 