Connected intersection of a closed filter base (source code)

= Connected intersection of a closed filter base
{title2=$\bigcap\mathcal F\ne\varnothing$}

A closed <filter base> in a <compact space> has nonempty <intersection>. If the space is Hausdorff and every base member is <connected>, the <intersection> is <connected>. Otherwise <normal space>[normality] separates its two closed components by disjoint <open sets>. <Compactness> of the complement supplies finitely many base members whose <intersection> lies in that <union>; directedness then gives a single base member meeting both sides, contradicting its <connected space>[connectedness].