1: \begin{definition}%{\textit{Invariant}\\}

2: We define the following \textit{invariant}:

3: Let $J_{\min}$ and $J_{\max}$ be minimal and maximal bases of $Y$.

4: \begin{align}

5: \forall a \in J_{\max}: J_{\min} \sqcap ball(a) \neq \emptyset \label{eq:DeletionInvariant}

6: \end{align}

7: This invariant captures the necessary condition to be able to delete every element in $J_{\max}$ eventually because for every such element we have an element in $J_{\min}$ that could still delete it. 

8: Next we show that this condition is actually invariant under the previously defined \textsc{DeletionStep}.

9: This means that we will be able to delete every element in $J_{\max}$ eventually (used in the proof of Theorem~\ref{theorem:layout_constraints_psystem}).

10: \end{definition}

11: