Soit $x$ un point de $X$. Soit $Q$ un voisinage de $f_{\text{trop}}(x)$ dans $f_{\text{trop}}(X)$ qui est un polytope compact. Le domaine analytique $W=f_{\text{trop}}^{-1}(Q)$ de $X$ est un voisinage de $x$ et $\omega|_{W}=(f|_{W})^{*}(\alpha|_{Q})$.

Supposons que $x$ appartienne à $K$. Le compact $K$ rencontre alors l’intérieur de $W$, ce qui entraîne que $\omega|_{W}\neq 0$, et donc que $\alpha|_{Q}\neq 0$. Il s’ensuit que $H$ rencontre $Q$. Comme $Q$ peut être choisi arbitrairement petit, $f_{\text{trop}}(x)$ appartient à $H$, d’où l’inclusion $f_{\text{trop}}(K)\subset H$.

Inversement, supposons que $f_{\text{trop}}(x)\in H$. Par définition de $H$, la restriction à $Q$ de la forme $\alpha$ est non nulle. Il s’ensuit d’après le lemme, que la restriction de $\omega$ à $f_{\text{trop}}^{-1}(Q)$ est non nulle. Par conséquent, $f_{\text{trop}}^{-1}(Q)$ rencontre $K$, et $Q=f_{\text{trop}}(f_{\text{trop}}^{-1}(Q))$ rencontre $f_{\text{trop}}(K)$. Comme $Q$ est un voisinage arbitrairement petit de $f_{\text{trop}}(x)$, celui-ci est adhérent à $f_{\text{trop}}(K)$. Puisque $f_{\text{trop}}(K)$ est compact, $f_{\text{trop}}(x)$ appartient à $f_{\text{trop}}(K)$. ∎