Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact

Suppose, for contradiction, that $[a,b]$ is not compact: some open cover $\mathcal{U}$ of $[a,b]$ has no finite subcover, that is, the pair $(a,b)\in X$ is bad.

Bisection rule: for $(u,v)\in X$ put $m:=(u+v)\cdot 2^{-1}$, so that $u\le m\le v$ by [L8], and define $G(u,v):=(u,m)$ if $(u,m)$ is bad and $G(u,v):=(m,v)$ otherwise. This is a definition by cases on one condition, so $G:X\to X$ is a function and nothing is selected.

If $(u,v)$ is bad then $G(u,v)$ is bad: were both $(u,m)$ and $(m,v)$ not bad, concatenating the two finite lists of members of $\mathcal{U}$ would give a finite subfamily whose union contains $[u,m]\cup [m,v]=[u,v]$ by [L2], so $(u,v)$ would not be bad; hence at least one half is bad, and the rule returns the left half when it is bad and otherwise the right half, which must then be bad.

Apply [L4] with $Y=X$, seed $(a,b)$ and map $G$: there is $h:\mathbb{N}\to X$ with $h(0)=(a,b)$ and $h(k+1)=G(h(k))$. Write $h(k)=(a_k,b_k)$, so $a_k\le b_k$ for every $k$, $(a_0,b_0)=(a,b)$, and $(a_{k+1},b_{k+1})$ is one of the two halves of $(a_k,b_k)$.

Every $(a_k,b_k)$ is bad, by induction on $k$: the case $k=0$ is step 1.1, and if $(a_k,b_k)$ is bad then $(a_{k+1},b_{k+1})=G(a_k,b_k)$ is bad by step 1.3.

Writing ${\mathrm{\ell }}_k:=b_k-a_k\ge 0$, the intervals are nested and the lengths halve: $[a_{k+1},b_{k+1}]$ is $[a_k,m_k]$ or $[m_k,b_k]$ with $m_k=(a_k+b_k)\cdot 2^{-1}$, and each of these is contained in $[a_k,b_k]$ by [L2], while $m_k-a_k=b_k-m_k={\mathrm{\ell }}_k\cdot 2^{-1}$, so ${\mathrm{\ell }}_{k+1}={\mathrm{\ell }}_k\cdot 2^{-1}$.

For every $k\in \mathbb{N}$ one has ${\mathrm{\ell }}_k\cdot (k+1)\le {\mathrm{\ell }}_0$, by induction on $k$: at $k=0$ this reads ${\mathrm{\ell }}_0\cdot 1\le {\mathrm{\ell }}_0$; and if it holds at $k$ then ${\mathrm{\ell }}_{k+1}\cdot (k+2)={\mathrm{\ell }}_k\cdot 2^{-1}\cdot (k+2)\le {\mathrm{\ell }}_k\cdot (k+1)\le {\mathrm{\ell }}_0$, using ${\mathrm{\ell }}_k\ge 0$ and $(k+2)\cdot 2^{-1}\le k+1$, which is $k+2\le 2k+2$, that is $0\le k$.

By [L5] the nested family $[a_k,b_k]$ of nonempty closed bounded intervals has a common point $x$; since $x\in [a_0,b_0]=[a,b]$ and $\mathcal{U}$ covers $[a,b]$, fix $U\in \mathcal{U}$ with $x\in U$ and then, $U$ being open, a real $\epsilon >0$ with $N_{\epsilon }(x)\subseteq U$.

There is $k\in \mathbb{N}$ with ${\mathrm{\ell }}_k<\epsilon$: the real $\epsilon \mathrm{/}({\mathrm{\ell }}_0+1)$ is positive because ${\mathrm{\ell }}_0+1>0$, so [L6] supplies a natural $n\ge 1$ with $1\mathrm{/}n<\epsilon \mathrm{/}({\mathrm{\ell }}_0+1)$; put $k:=n-1$, a natural number, so that $k+1=n$ and step 4.1 with [L7] gives ${\mathrm{\ell }}_k\le {\mathrm{\ell }}_0\cdot (1\mathrm{/}n)\le {\mathrm{\ell }}_0\cdot \epsilon \mathrm{/}({\mathrm{\ell }}_0+1)<\epsilon$, the last step because ${\mathrm{\ell }}_0<{\mathrm{\ell }}_0+1$ forces ${\mathrm{\ell }}_0\mathrm{/}({\mathrm{\ell }}_0+1)<1$ and $\epsilon >0$.

For that $k$ one has $x\in [a_k,b_k]$, and every $y\in [a_k,b_k]$ satisfies $\mathrm{\mid }y-x\mathrm{\mid }\le {\mathrm{\ell }}_k<\epsilon$ by [L9], so $[a_k,b_k]\subseteq N_{\epsilon }(x)\subseteq U$; hence the one-member subfamily $\{U\}$ of $\mathcal{U}$ covers $[a_k,b_k]$ and $(a_k,b_k)$ is not bad, contradicting step 3.1. The assumption of step 1.1 is therefore untenable and $[a,b]$ is compact.