Boundary-bumping theorem for compact subsets (source code)

= Boundary-bumping theorem for compact subsets
{title2=$D\subsetneq X,\quad D\text{ compact},\quad X\text{ connected Hausdorff}\Longrightarrow C\cap\partial D\ne\varnothing$}

Every <connected component> $C$ of a nonempty <compact> proper subset $D$ of a <connected> <Hausdorff space> meets its <boundary>. If not, the <Šura-Bura lemma> identifies $C$ as a <quasi-component> in the <compact> <Hausdorff> subspace $D$. Finitely many <clopen> <neighborhoods> separate it from the <compact> <boundary>, giving a nonempty relatively <clopen> $H\subseteq\operatorname{int}D$. Such $H$ is open in the ambient space, and is also closed there because $D$ is closed. It is proper because $D$ is proper. This contradicts <connectedness>.