Let X and Tx be given.
Assume HH: Hausdorff_space X Tx.
We will prove one_point_sets_closed X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
∎