Let X and Tx be given.
Assume Hreg: regular_space X Tx.
We will prove Hausdorff_space X Tx.
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).
We prove the intermediate claim Hsing: ∀x : set, x ∈ X → closed_in X Tx {x}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).
We prove the intermediate claim HSepReg: ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We will prove 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.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume Hneq: x1 ≠ x2.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hcl: closed_in X Tx {x2}.
An exact proof term for the current goal is (Hsing x2 Hx2X).
We prove the intermediate claim Hx1not: x1 ∉ {x2}.
Assume Hx1in: x1 ∈ {x2}.
We prove the intermediate claim Heq: x1 = x2.
An exact proof term for the current goal is (SingE x2 x1 Hx1in).
An exact proof term for the current goal is (Hneq Heq).
We prove the intermediate claim Hex: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ {x2} ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepReg x1 Hx1X {x2} Hcl Hx1not).
Set U0 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ {x2} ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU0ex: ∃V : set, U0 ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U0 ∧ {x2} ⊆ V ∧ U0 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ {x2} ⊆ V ∧ U ∩ V = Empty) Hex).
Set V0 to be the term Eps_i (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U0 ∧ {x2} ⊆ V ∧ U0 ∩ V = Empty).
We prove the intermediate claim HV0prop: U0 ∈ Tx ∧ V0 ∈ Tx ∧ x1 ∈ U0 ∧ {x2} ⊆ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U0 ∧ {x2} ⊆ V ∧ U0 ∩ V = Empty) HU0ex).
We prove the intermediate claim H1234: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0) ∧ {x2} ⊆ V0).
An exact proof term for the current goal is (andEL ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0) ∧ {x2} ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim HdisjUV: U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0) ∧ {x2} ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim H123: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0).
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0) ({x2} ⊆ V0) H1234).
We prove the intermediate claim H12: (U0 ∈ Tx ∧ V0 ∈ Tx).
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (x1 ∈ U0) H123).
We prove the intermediate claim HUx1: x1 ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (x1 ∈ U0) H123).
We prove the intermediate claim HVsub: {x2} ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x1 ∈ U0) ({x2} ⊆ V0) H1234).
We prove the intermediate claim Hx2V0: x2 ∈ V0.
Apply HVsub to the current goal.
An exact proof term for the current goal is (SingI x2).
We use U0 to witness the existential quantifier.
We use V0 to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).
An exact proof term for the current goal is HUx1.
An exact proof term for the current goal is Hx2V0.
An exact proof term for the current goal is HdisjUV.
∎