[proofplan] We collect the chosen sets $U_j$ into a finite subfamily of $\mathcal U$. Then we prove it covers $X$ by taking an arbitrary point $x \in X$, using the fact that $\mathcal W$ covers $X$ to place $x$ in some $W_j$, and then using the containment $W_j \subset U_j$. This verifies exactly the two requirements for a [finite subcover](/page/Finite%20Subcover): finiteness and coverage by members of the original cover. [/proofplan] [step:Collect the chosen sets into a finite subfamily of $\mathcal U$] Define the finite index set \begin{align*} J := \{1, \ldots, n\}. \end{align*} Define the chosen family \begin{align*} \mathcal V := \{U_j : j \in J\}. \end{align*} For every $j \in J$, the hypothesis gives $U_j \in \mathcal U$. Hence every element of $\mathcal V$ belongs to $\mathcal U$, so \begin{align*} \mathcal V \subset \mathcal U. \end{align*} Since $\mathcal V$ is indexed by the finite set $J$, it is finite. If some of the chosen sets $U_j$ coincide, the set notation defining $\mathcal V$ simply collapses repetitions, and the resulting family remains finite. [/step] [step:Use the finite cover $\mathcal W$ to show that $\mathcal V$ covers $X$] Let $x \in X$ be arbitrary. Since $\mathcal W = \{W_1, \ldots, W_n\}$ is a cover of $X$, there exists $j \in J$ such that $x \in W_j$. For this index $j$, the chosen refinement containment gives $W_j \subset U_j$, so $x \in U_j$. Since $U_j \in \mathcal V$, we have \begin{align*} x \in \bigcup_{V \in \mathcal V} V. \end{align*} Because $x \in X$ was arbitrary, it follows that \begin{align*} X \subset \bigcup_{V \in \mathcal V} V. \end{align*} [guided] We must prove that the chosen family $\mathcal V = \{U_j : j \in J\}$ covers every point of $X$. The natural way to prove a set inclusion is to start with an arbitrary point of the left-hand side. So let $x \in X$ be arbitrary. The only information that tells us where points of $X$ lie is that $\mathcal W = \{W_1, \ldots, W_n\}$ is a cover of $X$. By the definition of cover, this means that every point of $X$ lies in at least one member of $\mathcal W$. Therefore there exists an index $j \in J$ such that \begin{align*} x \in W_j. \end{align*} For this same index $j$, the hypothesis gives the containment \begin{align*} W_j \subset U_j. \end{align*} Membership is preserved under containment, so $x \in W_j$ and $W_j \subset U_j$ imply $x \in U_j$. By definition of $\mathcal V$, the set $U_j$ is one of the members of $\mathcal V$. Hence \begin{align*} x \in \bigcup_{V \in \mathcal V} V. \end{align*} Since the argument works for an arbitrary $x \in X$, we have proved the inclusion \begin{align*} X \subset \bigcup_{V \in \mathcal V} V. \end{align*} Thus $\mathcal V$ covers $X$. [/guided] [/step] [step:Conclude that the chosen family is a finite subcover] The family $\mathcal V = \{U_j : j \in J\}$ is finite and satisfies $\mathcal V \subset \mathcal U$. The previous step proved that $\mathcal V$ covers $X$. Therefore $\mathcal V$ is a finite subcover of $\mathcal U$. Since $\mathcal V = \{U_1, \ldots, U_n\}$, the family $\{U_1, \ldots, U_n\}$ is a finite subcover of $\mathcal U$. [/step]