Let X and Tx be given.
Assume HH: Hausdorff_space X Tx.
Let F be given.
Assume HFsub: F ⊆ X.
Assume HF: finite F.
We will prove closed_in X Tx F.
We prove the intermediate claim Htop: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
We prove the intermediate claim Hclosed_empty: closed_in X Tx Empty.
An exact proof term for the current goal is (empty_is_closed X Tx Htop).
We prove the intermediate claim Hall: ∀F0 : set, finite F0 → (F0 ⊆ X → closed_in X Tx F0).
An exact proof term for the current goal is (finite_ind (λF0 : set ⇒ F0 ⊆ X → closed_in X Tx F0) (λ_ ⇒ Hclosed_empty) (λF0 y : set ⇒ λHFin0 HyNotin IH ⇒ λHsubUnion ⇒ union_of_closed_is_closed X Tx F0 {y} Htop (IH (λz Hz ⇒ HsubUnion z (binunionI1 F0 {y} z Hz))) (Hausdorff_singletons_closed X Tx y HH (HsubUnion y (binunionI2 F0 {y} y (SingI y)))))).
An exact proof term for the current goal is ((Hall F HF) HFsub).
∎