[proofplan] We construct the refinement without making pointwise choices. Let $\mathcal V$ be the family of all basis elements that are contained in at least one member of the original cover $\mathcal U$. This definition immediately gives refinement, and the basis property ensures that every point of $X$ lies in some member of $\mathcal V$. [/proofplan] [step:Define the family of basis elements lying inside members of the cover] Define \begin{align*} \mathcal V := \{B \in \mathcal B : \text{there exists } U \in \mathcal U \text{ such that } B \subset U\}. \end{align*} By definition, $\mathcal V \subset \mathcal B$. Since $\mathcal B$ is a basis for $\tau$, every element of $\mathcal B$ belongs to $\tau$. Hence every $V \in \mathcal V$ is $\tau$-open. [/step] [step:Show that the basis family covers every point of $X$] Let $x \in X$. By the stated covering property of $\mathcal U$, there exists a set $U_x \in \mathcal U$ such that $x \in U_x$. Because $\mathcal U \subset \tau$, the set $U_x$ is $\tau$-open. Since $\mathcal B$ is a basis for $\tau$, applied to the [open set](/page/Open%20Set) $U_x$ and the point $x \in U_x$, there exists $B_x \in \mathcal B$ such that \begin{align*} x \in B_x \subset U_x. \end{align*} The containment $B_x \subset U_x$ with $U_x \in \mathcal U$ implies $B_x \in \mathcal V$. Therefore $x \in B_x$ for some $B_x \in \mathcal V$. As $x \in X$ was arbitrary, $\mathcal V$ covers $X$. [guided] Recall that \begin{align*} \mathcal V := \{B \in \mathcal B : \text{there exists } U \in \mathcal U \text{ such that } B \subset U\}. \end{align*} We need to prove that this family covers $X$. The non-immediate point is local: for an arbitrary point $x \in X$, we must find some basis element containing $x$ that is also contained in one member of $\mathcal U$. Fix $x \in X$. By the stated covering property of $\mathcal U$, there exists $U_x \in \mathcal U$ such that $x \in U_x$. Because the theorem assumes $\mathcal U \subset \tau$, this chosen set $U_x$ is open in the topology $\tau$. Now we use the defining property of a basis. Since $\mathcal B$ is a basis for $\tau$, whenever $O \in \tau$ and $y \in O$, there exists $B \in \mathcal B$ with $y \in B \subset O$. Apply this with $O = U_x$ and $y = x$. We obtain $B_x \in \mathcal B$ such that \begin{align*} x \in B_x \subset U_x. \end{align*} The definition of $\mathcal V$ was chosen precisely for this situation: a basis element belongs to $\mathcal V$ when it is contained in at least one member of $\mathcal U$. Since $B_x \subset U_x$ and $U_x \in \mathcal U$, we have $B_x \in \mathcal V$. Also $x \in B_x$, so the point $x$ is covered by $\mathcal V$. Because the argument works for every $x \in X$, the family $\mathcal V$ covers $X$. The same defining condition also gives refinement: if $V \in \mathcal V$, then by definition there exists $U \in \mathcal U$ such that $V \subset U$. [/guided] [/step] [step:Verify that the constructed cover refines the original cover] Let $V \in \mathcal V$. By the definition of $\mathcal V$, there exists $U \in \mathcal U$ such that $V \subset U$. Hence every member of $\mathcal V$ is contained in a member of $\mathcal U$, so $\mathcal V$ refines $\mathcal U$. Combining this with $\mathcal V \subset \mathcal B$ and the fact that $\mathcal V$ is an [open cover](/page/Open%20Cover) of $X$, we obtain the required basis refinement. [/step]