Let X and Tx be given.
Assume Hnorm: normal_space X Tx.
We will prove 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) (∀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 will prove 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.
Apply andI to the current goal.
An exact proof term for the current goal is HT1.
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hclx: closed_in X Tx {x}.
An exact proof term for the current goal is (Hsing x HxX).
We prove the intermediate claim Hdisj: {x} ∩ F = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ {x} ∩ F.
We will prove z ∈ Empty.
We prove the intermediate claim Hz1: z ∈ {x}.
An exact proof term for the current goal is (binintersectE1 {x} F z Hz).
We prove the intermediate claim Hz2: z ∈ F.
An exact proof term for the current goal is (binintersectE2 {x} F z Hz).
We prove the intermediate claim Hzx: z = x.
An exact proof term for the current goal is (SingE x z Hz1).
We prove the intermediate claim HxinF: x ∈ F.
rewrite the current goal using Hzx (from right to left).
An exact proof term for the current goal is Hz2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotF HxinF).
We prove the intermediate claim Hex: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U ∧ F ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepNorm {x} F Hclx HFcl Hdisj).
Set U0 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U ∧ F ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU0ex: ∃V : set, U0 ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U0 ∧ F ⊆ V ∧ U0 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hex).
Set V0 to be the term Eps_i (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U0 ∧ F ⊆ V ∧ U0 ∩ V = Empty).
We prove the intermediate claim HV0prop: U0 ∈ Tx ∧ V0 ∈ Tx ∧ {x} ⊆ U0 ∧ F ⊆ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ {x} ⊆ U0 ∧ F ⊆ V ∧ U0 ∩ V = Empty) HU0ex).
We prove the intermediate claim H1234: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ {x} ⊆ U0) ∧ F ⊆ V0).
An exact proof term for the current goal is (andEL ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ {x} ⊆ U0) ∧ F ⊆ 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) ∧ {x} ⊆ U0) ∧ F ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim H123: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ {x} ⊆ U0).
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ {x} ⊆ U0) (F ⊆ 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) ({x} ⊆ U0) H123).
We prove the intermediate claim Hsubx: {x} ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) ({x} ⊆ U0) H123).
We prove the intermediate claim HFsub: F ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ {x} ⊆ U0) (F ⊆ V0) H1234).
We prove the intermediate claim HxU0: x ∈ U0.
Apply Hsubx to the current goal.
An exact proof term for the current goal is (SingI x).
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 HxU0.
An exact proof term for the current goal is HFsub.
An exact proof term for the current goal is HdisjUV.
∎