Let X and d be given.

Assume Hc: complete_metric_space X d.

We will prove Baire_space X (metric_topology X d).

We prove the intermediate claim HBc: Baire_space_closed X (metric_topology X d).

An exact proof term for the current goal is (Baire_category_complete_metric_closed X d Hc).

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

∎