Let X and Tx be given.
Assume Hcomp: compact_space X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove Baire_space_closed X Tx.
We will prove topology_on X Tx ∧ ∀Fam : set, countable_set Fam → (∀A : set, A ∈ Fam → closed_in X Tx A ∧ interior_of X Tx A = Empty) → interior_of X Tx (⋃ Fam) = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
Let Fam be given.
Assume Hcount: countable_set Fam.
Assume Hclint: ∀A : set, A ∈ Fam → closed_in X Tx A ∧ interior_of X Tx A = Empty.
We will prove interior_of X Tx (⋃ Fam) = Empty.
An exact proof term for the current goal is (Baire_category_compact_Hausdorff_closed_core X Tx Fam Hcomp HH Hcount Hclint).
∎