Let X, Tx, A and B be given.
Assume Hnorm: normal_space X Tx.
Assume HA: closed_in X Tx A.
Assume HB: closed_in X Tx B.
Assume Hdisj: A ∩ B = Empty.
We will prove ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ closure_of X Tx U ∩ closure_of X Tx V = Empty.
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) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ 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}) HT1).
We prove the intermediate claim HSepNorm: ∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnorm).
We prove the intermediate claim Hex1: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepNorm A B HA HB Hdisj).
Set U0 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU0ex: ∃V : set, U0 ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V ∧ U0 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hex1).
Set V0 to be the term Eps_i (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V ∧ U0 ∩ V = Empty).
We prove the intermediate claim HV0prop: U0 ∈ Tx ∧ V0 ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U0 ∧ B ⊆ V ∧ U0 ∩ V = Empty) HU0ex).
We prove the intermediate claim H1234: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0).
An exact proof term for the current goal is (andEL ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim Hdisj0: U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) ∧ B ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim H123: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0).
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ 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) (A ⊆ U0) H123).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HAsub: A ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (A ⊆ U0) H123).
We prove the intermediate claim HBsub: B ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ A ⊆ U0) (B ⊆ V0) H1234).
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (PowerE X U0 (HTsub U0 HU0Tx)).
We prove the intermediate claim HclU0: closed_in X Tx (closure_of X Tx U0).
An exact proof term for the current goal is (closure_is_closed X Tx U0 HTx HU0subX).
We prove the intermediate claim Hcliff0: ∀z : set, z ∈ X → (z ∈ closure_of X Tx U0 ↔ (∀W ∈ Tx, z ∈ W → W ∩ U0 ≠ Empty)).
Let z be given.
Assume HzX: z ∈ X.
An exact proof term for the current goal is (closure_characterization X Tx U0 z HTx HzX).
We prove the intermediate claim HclU0_disj_V0: closure_of X Tx U0 ∩ V0 = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ closure_of X Tx U0 ∩ V0.
We will prove z ∈ Empty.
We prove the intermediate claim Hzcl: z ∈ closure_of X Tx U0.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx U0) V0 z Hz).
We prove the intermediate claim HzV: z ∈ V0.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx U0) V0 z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀W : set, W ∈ Tx → z0 ∈ W → W ∩ U0 ≠ Empty) z Hzcl).
We prove the intermediate claim Hneigh: ∀W ∈ Tx, z ∈ W → W ∩ U0 ≠ Empty.
An exact proof term for the current goal is (iffEL (z ∈ closure_of X Tx U0) (∀W ∈ Tx, z ∈ W → W ∩ U0 ≠ Empty) (Hcliff0 z HzX) Hzcl).
We prove the intermediate claim Hcontr: V0 ∩ U0 ≠ Empty.
An exact proof term for the current goal is (Hneigh V0 HV0Tx HzV).
We prove the intermediate claim Hempty: V0 ∩ U0 = Empty.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ V0 ∩ U0.
We will prove w ∈ Empty.
We prove the intermediate claim HwV: w ∈ V0.
An exact proof term for the current goal is (binintersectE1 V0 U0 w Hw).
We prove the intermediate claim HwU: w ∈ U0.
An exact proof term for the current goal is (binintersectE2 V0 U0 w Hw).
We prove the intermediate claim HwUV: w ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 w HwU HwV).
We prove the intermediate claim HwE: w ∈ Empty.
rewrite the current goal using Hdisj0 (from right to left).
An exact proof term for the current goal is HwUV.
An exact proof term for the current goal is HwE.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontr Hempty).
We prove the intermediate claim HBcldisj: B ∩ closure_of X Tx U0 = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ B ∩ closure_of X Tx U0.
We will prove z ∈ Empty.
We prove the intermediate claim HzB: z ∈ B.
An exact proof term for the current goal is (binintersectE1 B (closure_of X Tx U0) z Hz).
We prove the intermediate claim Hzcl: z ∈ closure_of X Tx U0.
An exact proof term for the current goal is (binintersectE2 B (closure_of X Tx U0) z Hz).
We prove the intermediate claim HzV0: z ∈ V0.
Apply HBsub to the current goal.
An exact proof term for the current goal is HzB.
We prove the intermediate claim HzclV0: z ∈ closure_of X Tx U0 ∩ V0.
An exact proof term for the current goal is (binintersectI (closure_of X Tx U0) V0 z Hzcl HzV0).
We prove the intermediate claim HzE: z ∈ Empty.
rewrite the current goal using HclU0_disj_V0 (from right to left).
An exact proof term for the current goal is HzclV0.
An exact proof term for the current goal is HzE.
We prove the intermediate claim Hex2: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepNorm B (closure_of X Tx U0) HB HclU0 HBcldisj).
Set U1 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU1ex: ∃V : set, U1 ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty) Hex2).
Set V1 to be the term Eps_i (λV : set ⇒ U1 ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty).
We prove the intermediate claim HV1prop: U1 ∈ Tx ∧ V1 ∈ Tx ∧ B ⊆ U1 ∧ closure_of X Tx U0 ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U1 ∈ Tx ∧ V ∈ Tx ∧ B ⊆ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty) HU1ex).
We prove the intermediate claim H1234b: (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1) ∧ closure_of X Tx U0 ⊆ V1).
An exact proof term for the current goal is (andEL ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1) ∧ closure_of X Tx U0 ⊆ V1)) (U1 ∩ V1 = Empty) HV1prop).
We prove the intermediate claim Hdisj1: U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1) ∧ closure_of X Tx U0 ⊆ V1)) (U1 ∩ V1 = Empty) HV1prop).
We prove the intermediate claim H123b: ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1).
An exact proof term for the current goal is (andEL ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1) (closure_of X Tx U0 ⊆ V1) H1234b).
We prove the intermediate claim H12b: (U1 ∈ Tx ∧ V1 ∈ Tx).
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ V1 ∈ Tx) (B ⊆ U1) H123b).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (V1 ∈ Tx) H12b).
We prove the intermediate claim HV1Tx: V1 ∈ Tx.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (V1 ∈ Tx) H12b).
We prove the intermediate claim HBsubU1: B ⊆ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ V1 ∈ Tx) (B ⊆ U1) H123b).
We prove the intermediate claim HclU0subV1: closure_of X Tx U0 ⊆ V1.
An exact proof term for the current goal is (andER ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ B ⊆ U1) (closure_of X Tx U0 ⊆ V1) H1234b).
We prove the intermediate claim Hcliff1: ∀z : set, z ∈ X → (z ∈ closure_of X Tx U1 ↔ (∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty)).
Let z be given.
Assume HzX: z ∈ X.
An exact proof term for the current goal is (closure_characterization X Tx U1 z HTx HzX).
We prove the intermediate claim Hcldisj: closure_of X Tx U0 ∩ closure_of X Tx U1 = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ closure_of X Tx U0 ∩ closure_of X Tx U1.
We will prove z ∈ Empty.
We prove the intermediate claim Hzcl0: z ∈ closure_of X Tx U0.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx U0) (closure_of X Tx U1) z Hz).
We prove the intermediate claim Hzcl1: z ∈ closure_of X Tx U1.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx U0) (closure_of X Tx U1) z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀W : set, W ∈ Tx → z0 ∈ W → W ∩ U0 ≠ Empty) z Hzcl0).
We prove the intermediate claim HzV1: z ∈ V1.
Apply HclU0subV1 to the current goal.
An exact proof term for the current goal is Hzcl0.
We prove the intermediate claim Hneigh: ∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty.
An exact proof term for the current goal is (iffEL (z ∈ closure_of X Tx U1) (∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty) (Hcliff1 z HzX) Hzcl1).
We prove the intermediate claim Hcontr: V1 ∩ U1 ≠ Empty.
An exact proof term for the current goal is (Hneigh V1 HV1Tx HzV1).
We prove the intermediate claim Hempty: V1 ∩ U1 = Empty.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ V1 ∩ U1.
We will prove w ∈ Empty.
We prove the intermediate claim HwV: w ∈ V1.
An exact proof term for the current goal is (binintersectE1 V1 U1 w Hw).
We prove the intermediate claim HwU: w ∈ U1.
An exact proof term for the current goal is (binintersectE2 V1 U1 w Hw).
We prove the intermediate claim HwUV: w ∈ U1 ∩ V1.
An exact proof term for the current goal is (binintersectI U1 V1 w HwU HwV).
We prove the intermediate claim HwE: w ∈ Empty.
rewrite the current goal using Hdisj1 (from right to left).
An exact proof term for the current goal is HwUV.
An exact proof term for the current goal is HwE.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontr Hempty).
We use U0 to witness the existential quantifier.
We use U1 to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (andI (topology_on X Tx) (U0 ∈ Tx) HTx HU0Tx).
An exact proof term for the current goal is (andI (topology_on X Tx) (U1 ∈ Tx) HTx HU1Tx).
An exact proof term for the current goal is HAsub.
An exact proof term for the current goal is HBsubU1.
An exact proof term for the current goal is Hcldisj.
∎