Let X, Tx and x be given.
Assume HH: Hausdorff_space X Tx.
Assume HxX: x ∈ X.
We will prove closed_in X Tx {x}.
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 HxSub: {x} ⊆ X.
Let y be given.
Assume Hy: y ∈ {x}.
We prove the intermediate claim Hyeq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim HUopen: X ∖ {x} ∈ Tx.
An exact proof term for the current goal is (Hausdorff_singleton_complement_open X Tx x HH HxX).
We prove the intermediate claim Hclosed: closed_in X Tx (X ∖ (X ∖ {x})).
An exact proof term for the current goal is (closed_of_open_complement X Tx (X ∖ {x}) Htop HUopen).
We prove the intermediate claim Heq: X ∖ (X ∖ {x}) = {x}.
An exact proof term for the current goal is (setminus_setminus_eq X {x} HxSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hclosed.
∎