Assume HH: Hausdorff_space X Tx.

We will prove Hausdorff_space X Tx'.

We prove the intermediate claim HSep: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ 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) HH).

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 Hex: ∃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 Hx1X Hx2X Hneq).

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 HVx2: 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 HU0Tx': U0 ∈ Tx'.

Apply Hfiner to the current goal.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).

We prove the intermediate claim HV0Tx': V0 ∈ Tx'.

Apply Hfiner to the current goal.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).

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 HU0Tx'.

An exact proof term for the current goal is HV0Tx'.

An exact proof term for the current goal is HUx1.

An exact proof term for the current goal is HVx2.

An exact proof term for the current goal is HdisjUV.

An exact proof term for the current goal is Hhaus_finer.

We will prove regular_space X Tx → Hausdorff_space X Tx'.

Assume Hreg: regular_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 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 prove the intermediate claim HHcoarse: Hausdorff_space X Tx.

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 (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).

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.

An exact proof term for the current goal is (Hhaus_finer HHcoarse).

We will prove normal_space X Tx → Hausdorff_space X Tx'.

Assume Hnorm: normal_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) (∀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 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 HSepNorm: ∀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 HHcoarse: Hausdorff_space X Tx.

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 (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).

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 Hex: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ {x1} ⊆ U ∧ {x2} ⊆ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (HSepNorm {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) 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 Hsub1: {x1} ⊆ U0.

An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) ({x1} ⊆ U0) H123).

We prove the intermediate claim Hsub2: {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 Hx1U0: x1 ∈ U0.

Apply Hsub1 to the current goal.

An exact proof term for the current goal is (SingI x1).

We prove the intermediate claim Hx2V0: x2 ∈ V0.

Apply Hsub2 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 Hx1U0.

An exact proof term for the current goal is Hx2V0.

An exact proof term for the current goal is HdisjUV.

An exact proof term for the current goal is (Hhaus_finer HHcoarse).