The Finite Intersection Property of a Compact Set

In the setting of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(X,\mathcal{T})$ be a topological space, let $K\subseteq X$ be compact in $(X,\mathcal{T})$, let $I$ be a nonempty set, and let $(F_{i})_{i\in I}$ be a family of subsets of $X$, each closed in $(X,\mathcal{T})$. For nonempty $J\subseteq I$, $\bigcap_{i\in J}F_{i}$ is the intersection of the family $(F_{i})_{i\in J}$.

(i) Finite intersections. If

$$K\cap\bigcap_{i\in J}F_{i}\neq\emptyset$$

for every nonempty finite subset $J$ of $I$, then

$$K\cap\bigcap_{i\in I}F_{i}\neq\emptyset.$$