1: \begin{definition}\label{PROP_DeltaPowerset}

2: Let $\mb{A} = \langle A,a_I,\Delta,\Omega\rangle$ be a $\wmso$-automaton. Let $c \in C$ be a label and $Q \in \shA$ a binary relation on $A$. By Theorem \ref{thm:bfolque} there is a sentence $\Psi_{Q,c} \in \olque(A\times A)$ in basic form such that

3: \begin{eqnarray*}

4: % \nonumber to remove numbering (before each equation)

5:   \bigwedge_{a \in \m{Ran}(Q)} \Delta^{\star}(a,c) &\equiv& \Psi_{Q,c}.

6: \end{eqnarray*}

7: By definition $\Psi_{Q,c}$ is of the form $\bigvee_{1\leq i\leq k}\varphi_i$. We put $\shDe(Q,c) := \bigvee_{1\leq i\leq k}\varphi_i^{\f}$, where the translation $(-)^{\f}$ is given as in definition \ref{DEF_finitary_lifting}. Observe that $\shDe(Q,c)$ is of type $\olque(A \cup \shA)$.

8: \end{definition}

9: