Let X and Tx be given.
Assume Hnorm: normal_space X Tx.
Assume HT1: T1_space X Tx.
We will prove Hausdorff_space X Tx.
We prove the intermediate claim HT1part: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
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}) HT1part).
We prove the intermediate claim Hsing: ∀x : set, x ∈ X → closed_in X Tx {x}.
An exact proof term for the current goal is (iffEL (T1_space X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) (lemma_T1_singletons_closed X Tx HTx) HT1).
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 Hcl1: closed_in X Tx {x1}.
An exact proof term for the current goal is (Hsing x1 Hx1X).
We prove the intermediate claim Hcl2: closed_in X Tx {x2}.
An exact proof term for the current goal is (Hsing x2 Hx2X).
We prove the intermediate claim Hdisj: {x1} ∩ {x2} = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ {x1} ∩ {x2}.
We will prove z ∈ Empty.
We prove the intermediate claim Hz1: z ∈ {x1}.
An exact proof term for the current goal is (binintersectE1 {x1} {x2} z Hz).
We prove the intermediate claim Hz2: z ∈ {x2}.
An exact proof term for the current goal is (binintersectE2 {x1} {x2} z Hz).
We prove the intermediate claim Hzx1: z = x1.
An exact proof term for the current goal is (SingE x1 z Hz1).
We prove the intermediate claim Hzx2: z = x2.
An exact proof term for the current goal is (SingE x2 z Hz2).
We prove the intermediate claim Hx1x2: x1 = x2.
rewrite the current goal using Hzx1 (from right to left).
rewrite the current goal using Hzx2 (from left to right).
Use reflexivity.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Hx1x2).
We prove the intermediate claim Hsep: ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ {x1} ⊆ U ∧ {x2} ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep {x1} {x2} Hcl1 Hcl2 Hdisj).
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) HexUV).
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 Hs2: {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 Hab: 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 HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) Hab).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) Hab).
We prove the intermediate claim Hs1: {x1} ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) ({x1} ⊆ U0) H123).
We prove the intermediate claim Hx1U0: x1 ∈ U0.
An exact proof term for the current goal is (Hs1 x1 (SingI x1)).
We prove the intermediate claim Hx2V0: x2 ∈ V0.
An exact proof term for the current goal is (Hs2 x2 (SingI x2)).
We use U0 to witness the existential quantifier.
We use V0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Tx.
An exact proof term for the current goal is HV0Tx.
An exact proof term for the current goal is Hx1U0.
An exact proof term for the current goal is Hx2V0.
An exact proof term for the current goal is HdisjUV.
∎