The proof constructs $f$ explicitly using the normality of $X$ to build a family of open and [closed sets](/page/Closed%20Set) indexed by dyadic rationals, then defines $f$ as an infimum over these indices. **Step 1: Iterative construction of nested [sets](/page/Set).** Set $U_1 := X \setminus C_1$, which is open with $C_0 \subset U_1$. By normality, there exist closed $C_{1/2}$ and open $U_{1/2}$ with $C_0 \subset U_{1/2} \subset C_{1/2} \subset U_1$. Repeating: for each dyadic rational $q = a/2^n$ with $a \in \{1, \ldots, 2^n - 1\}$ and $n \in \mathbb{N}$, construct open $U_q$ and closed $C_q$ such that $U_q \subset C_q$ and $C_q \subset U_{q'}$ whenever $q < q'$. **Step 2: Define $f$.** Set $f(x) := \inf\{q \in (0, 1] \text{ dyadic} : x \in U_q\}$ with the convention $\inf(\varnothing) = 1$. **Step 3: Verify the [boundary](/page/Boundary) conditions.** If $x \in C_0$, then $x \in U_q$ for all dyadic $q \in (0, 1]$, so $f(x) = 0$. If $x \in C_1$, then $x \notin U_q$ for any dyadic $q \in (0, 1)$ (since $C_q \subset U_1 = X \setminus C_1$), so $f(x) = 1$. By construction, $0 \le f \le 1$. **Step 4: [Continuity](/page/Continuity).** For $\alpha \in \mathbb{R}$: $\{x : f(x) < \alpha\} = \bigcup_{q < \alpha} U_q$ (a union of [open sets](/page/Open%20Set), hence open) and $\{x : f(x) > \alpha\} = \bigcup_{q > \alpha} (X \setminus C_q)$ (a union of open sets, hence open). Since the preimage of every open interval is open, and open intervals generate the [topology](/page/Topology) on $\mathbb{R}$, $f$ is continuous.