The endpoint of a lifted path depends only on its endpoint-fixed homotopy class

Given: The objects, hypotheses, and choice principles stated above.

Let $p:E\to B$ be a covering, $H:Y\times I\to B$ a homotopy, and ${\tilde{H}}_0:Y\to E$ a lift of $H(-,0)$. There is a unique lift $\tilde{H}:Y\times I\to E$ of $H$ extending ${\tilde{H}}_0$. (Existence and uniqueness of homotopy lifts through a covering map).

Every covering map is a surjective local homeomorphism, and each of its fibres is discrete in the subspace topology. (Covering maps are surjective local homeomorphisms with discrete fibres).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space). A separation of $X$ is an ordered pair $(U,V)$ of open, nonempty, disjoint subsets of $X$ with $U\cup V=X$; $X$ is disconnected when a separation of $X$ exists and connected when none does. Since $U$ and $V$ are complementary each is clopen, so a separation is the same thing as a partition of $X$ into two nonempty clopen pieces. A subset $A\subseteq X$ is a connected subset when the subspace $(A,{\mathcal{T}}_A)$ is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).