Let X, Tx, x1 and x2 be given.
Assume H: Hausdorff_space X Tx.
Assume Hx1: x1 ∈ X.
Assume Hx2: x2 ∈ X.
Assume Hneq: x1 ≠ x2.
We prove the intermediate claim Hsep: ∀a b : set, a ∈ X → b ∈ X → a ≠ b → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) H).
An exact proof term for the current goal is (Hsep x1 x2 Hx1 Hx2 Hneq).
∎