Let X and Tx be given.

Assume Hcomp: compact_space X Tx.

Assume HH: Hausdorff_space X Tx.

We will prove Baire_space X Tx.

We prove the intermediate claim HBc: Baire_space_closed X Tx.

An exact proof term for the current goal is (Baire_category_compact_Hausdorff_closed X Tx Hcomp HH).

An exact proof term for the current goal is (Baire_space_closed_imp X Tx HBc).

∎