diff --git a/thesis/chapters/graph_simulator.tex b/thesis/chapters/graph_simulator.tex
index faadef5..c044661 100644
--- a/thesis/chapters/graph_simulator.tex
+++ b/thesis/chapters/graph_simulator.tex
@@ -240,11 +240,33 @@ were derived from the vertex operator-free graph states.
     \end{equation}
 
     as $X$, $Z$ anticommute.
-
 \end{proof}
 
+\begin{lemma}
+    \begin{equation}
+        \ket{\overline{G}} = \left(\prod\limits_{\{i,j\} \in E} CZ_{i,j} \right) \left(\prod\limits_{l \in V} H_l\right) \ket{0}
+    \end{equation}
 
+    In particular definitions \ref{def:vop_free_g_state} and \ref{def:graph_state} are consistent, when there are no 
+    vertex operators on the graph state $\ket{G}$.
+\end{lemma}
+\begin{proof}
+    Let $\ket{+} := \left(\prod\limits_{l \in V} H_l\right) \ket{0}$ as before. Note that for any $X_i$ $X_i \ket{+} = +1 \ket{+}$.
+    Set $\ket{\tilde{G}} := \left(\prod\limits_{\{i,j\} \in E} CZ_{i,j} \right)\ket{+}$.
 
+    \begin{equation}
+        \begin{aligned}
+            K_G^{(i)} \ket{\tilde{G}} & = X_i \left(\prod\limits_{\{i,j\} \in E} Z_j\right)\left(\prod\limits_{\{l,j\} \in E} CZ_{l,j} \right) \ket{+} \\
+            & = \left(\prod\limits_{\{i,j\} \in E} Z_j\right)X_i\prod\limits_{\{l,j\} \in E}\left( \ket{0}\bra{0}_j \otimes I_l + \ket{1}\bra{1}_j \otimes Z_l\right) \ket{+} \\
+            & = \left(\prod\limits_{\{i,j\} \in E} Z_j\right)\prod\limits_{\{l,j\} \in E}\left( \ket{0}\bra{0}_j \otimes I_l + (-1)^{\delta_{i,l}}\ket{1}\bra{1}_j \otimes Z_l\right) X_i \ket{+} \\
+            & = \prod\limits_{\{l,j\} \in E}\left( \ket{0}\bra{0}_j \otimes I_l + (-1)^{2\delta_{i,l}}\ket{1}\bra{1}_j \otimes Z_l\right) \ket{+} \\
+			& = \prod\limits_{\{l,j\} \in E}\left( \ket{0}\bra{0}_j \otimes I_l + \ket{1}\bra{1}_j \otimes Z_l\right) \ket{+} \\	
+		    & = +1 \ket{\tilde{G}}	
+        \end{aligned}
+    \end{equation}
+
+    as $X, Z$ anticommute and $Z\ket{1} = -1\ket{1}$.
+\end{proof}