Take
x(⇝,⇒)y. Then exists a path of elements of
A along the grid
If we choose a path of size
zero, then
x=y and so by reflexivity of
⇒ we get the chain
x⇒y
completing the proof.
To address paths of nonzero size, we will proceed by choosing a specific example path on which to work; the choice path will be generic enough to easily extend to a proof
covering all cases.
We choose this path:
now, in left-to-right
order, we repeatedly apply transitivity of
⇒ to obtain the following cyan-colored arrows, and repeatedly apply the lifting condition to obtain the following red-colored arrows:
In the end what we produce is a chain
x⇝∙⇝∙⇝⋯⇝∙⇒y
just as we desired