Gluing plugs (Béguin–Bonatti–Yu, Prop. 1.1): the maximal invariant set of the glued field is contained in Λ_X ∪ Λ_Y ∪ (connecting orbits)

Let $(U,X)$ and $(V,Y)$ be plugs: $X$, $Y$ are nonsingular C¹ vector fields on the compact 3-manifolds with boundary $U$, $V$, transverse to the boundary. Let $T^{out}$ be a union of connected components of the exit boundary $\partial^{out}U$, let $T^{in}$ be a union of connected components of the entrance boundary $\partial^{in}V$, and let $\varphi:T^{out}\to T^{in}$ be a C¹ diffeomorphism. Let $(W,Z)$ be a gluing of $(U,X)$ and $(V,Y)$ along $\varphi$: C¹ embeddings $i_U:U\to W$ and $i_V:V\to W$ with injective derivatives cover the compact 3-manifold $W$, identify exactly the points $x\in T^{out}$ with $\varphi(x)$, and satisfy $Di_U(X)=Z\circ i_U$, $Di_V(Y)=Z\circ i_V$. Write $\Lambda_X$, $\Lambda_Y$, $\Lambda_Z$ for the maximal invariant sets (points whose orbit is defined for all times), $L^u_X=W^u(\Lambda_X)\cap\partial^{out}U$ for the exit lamination of $(U,X)$ and $L^s_Y=W^s(\Lambda_Y)\cap\partial^{in}V$ for the entrance lamination of $(V,Y)$. Here $W^s(\Lambda_Y)$ is the stable set: the points of $V$ whose forward orbit is defined for all positive times; $W^u(\Lambda_X)$ is the unstable set: the points of $U$ whose backward orbit is defined for all negative times. The connecting set $\mathcal C\subseteq W$ is the $Z$-orbit of $\varphi_*(L^u_X)\cap L^s_Y$: the set of points $w$ that lie on a complete integral curve $\gamma:\mathbb R\to W$ of $Z$ with $\gamma(0)=i_U(x)=i_V(\varphi(x))$ for some $x\in L^u_X\cap T^{out}$ with $\varphi(x)\in L^s_Y$. Then every point of the maximal invariant set of $Z$ lies in one of the three pieces:

This is the inclusion $\subseteq$ in the sentence "$\Lambda_Z$ is the union of $\Lambda_X$, $\Lambda_Y$ and the $Z$-orbit of $\varphi_*(L^u_X)\cap L^s_Y$" of the proof of Proposition 1.1.

Formalization Note Only the plug hypotheses on $X$ and $Y$ are assumed (not hyperbolicity). $Z$ is not assumed to be C¹; it is controlled only through the embeddings. The connecting set is phrased by the existence of a complete integral curve of $Z$ through the gluing point, not through a flow map, because uniqueness of integral curves of $Z$ is not among the hypotheses. The hypotheses on $\varphi$, $T^{out}$ and $T^{in}$ are those of Proposition 1.1. The maximal invariant set, the stable set and the unstable set are defined by integral curves in the sense of Mathlib's IsMIntegralCurve / IsMIntegralCurveOn (one-sided derivatives at interval endpoints).