Opposite crossings of a rectangular grid intersect

Delete loops from each finite path until it is simple, preserving its endpoints. In the square grid, two unit edges can meet only at a shared endpoint, so if the paths do not share a vertex their polygonal realizations are disjoint compact sets. Their distance is then positive.

Suppose the paths are disjoint and denote the simple left-to-right path by $\gamma$. Perturb its finitely many interior vertices and boundary contacts by less than one third of the distance in step 1.1, pushing every nonendpoint boundary contact slightly into the rectangle. Since $\gamma$ is a finite simple polygonal arc, choose disjoint small neighborhoods of its nonadjacent segments; local polygonal detours inside those neighborhoods preserve simplicity, keep its endpoints on the left and right sides, and preserve disjointness from the other path. The resulting simple arc $\tilde{\gamma }$ meets the rectangle boundary only at its two endpoints.

Join the endpoints of $\tilde{\gamma }$ by a simple polygonal arc lying outside the rectangle and running around its top side. Their union is a simple polygonal closed curve by the boundary-contact property in step 2.1. By [F1], its bounded component contains the part of the rectangle immediately below the top side and above $\tilde{\gamma }$, while the bottom side lies in the unbounded component. A bottom-to-top path staying in the rectangle must therefore cross this Jordan curve; it cannot meet the outside closing arc, so it must meet $\tilde{\gamma }$. This contradicts the preserved disjointness in step 2.1. Thus the original paths intersect; grid edges intersect only at shared vertices, proving the claim.