Assume HT1: one_point_sets_closed X Tx.

We will prove regular_space X Tx ↔ ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U.

Apply iffI to the current goal.

Assume Hreg: regular_space X Tx.

We will prove ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U.

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).

Let x and U be given.

Assume HxX: x ∈ X.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

Set B to be the term X ∖ U.

We prove the intermediate claim HBcl: closed_in X Tx B.

An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HU).

We prove the intermediate claim HxnotB: x ∉ B.

Assume HxB: x ∈ B.

We prove the intermediate claim HxnotU: x ∉ U.

An exact proof term for the current goal is (setminusE2 X U x HxB).

An exact proof term for the current goal is (HxnotU HxU).

We prove the intermediate claim Hex: ∃V W : set, V ∈ Tx ∧ W ∈ Tx ∧ x ∈ V ∧ B ⊆ W ∧ V ∩ W = Empty.

An exact proof term for the current goal is (HSepReg x HxX B HBcl HxnotB).

Set V0 to be the term Eps_i (λV : set ⇒ ∃W : set, V ∈ Tx ∧ W ∈ Tx ∧ x ∈ V ∧ B ⊆ W ∧ V ∩ W = Empty).

We prove the intermediate claim HV0ex: ∃W : set, V0 ∈ Tx ∧ W ∈ Tx ∧ x ∈ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ ∃W : set, V ∈ Tx ∧ W ∈ Tx ∧ x ∈ V ∧ B ⊆ W ∧ V ∩ W = Empty) Hex).

Set W0 to be the term Eps_i (λW : set ⇒ V0 ∈ Tx ∧ W ∈ Tx ∧ x ∈ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty).

We prove the intermediate claim HW0prop: V0 ∈ Tx ∧ W0 ∈ Tx ∧ x ∈ V0 ∧ B ⊆ W0 ∧ V0 ∩ W0 = Empty.

An exact proof term for the current goal is (Eps_i_ex (λW : set ⇒ V0 ∈ Tx ∧ W ∈ Tx ∧ x ∈ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty) HV0ex).

We prove the intermediate claim H1234: (((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0) ∧ B ⊆ W0).

An exact proof term for the current goal is (andEL ((((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0) ∧ B ⊆ W0)) (V0 ∩ W0 = Empty) HW0prop).

We prove the intermediate claim HdisjVW: V0 ∩ W0 = Empty.

An exact proof term for the current goal is (andER ((((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0) ∧ B ⊆ W0)) (V0 ∩ W0 = Empty) HW0prop).

We prove the intermediate claim H123: ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0).

An exact proof term for the current goal is (andEL ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0) (B ⊆ W0) H1234).

We prove the intermediate claim H12: (V0 ∈ Tx ∧ W0 ∈ Tx).

An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ W0 ∈ Tx) (x ∈ V0) H123).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

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

We prove the intermediate claim HW0Tx: W0 ∈ Tx.

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

We prove the intermediate claim HxV0: x ∈ V0.

An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ W0 ∈ Tx) (x ∈ V0) H123).

We prove the intermediate claim HBsubW0: B ⊆ W0.

An exact proof term for the current goal is (andER ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ x ∈ V0) (B ⊆ W0) H1234).

We prove the intermediate claim HdisjWV: W0 ∩ V0 = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ W0 ∩ V0.

We will prove z ∈ Empty.

We prove the intermediate claim HzW: z ∈ W0.

An exact proof term for the current goal is (binintersectE1 W0 V0 z Hz).

We prove the intermediate claim HzV: z ∈ V0.

An exact proof term for the current goal is (binintersectE2 W0 V0 z Hz).

We prove the intermediate claim HzVW: z ∈ V0 ∩ W0.

An exact proof term for the current goal is (binintersectI V0 W0 z HzV HzW).

We prove the intermediate claim HzE: z ∈ Empty.

rewrite the current goal using HdisjVW (from right to left).

An exact proof term for the current goal is HzVW.

An exact proof term for the current goal is HzE.

We prove the intermediate claim HclV0subU: closure_of X Tx V0 ⊆ U.

Let z be given.

Assume Hzcl: z ∈ closure_of X Tx V0.

We will prove z ∈ U.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀N : set, N ∈ Tx → z0 ∈ N → N ∩ V0 ≠ Empty) z Hzcl).

Apply xm (z ∈ U) to the current goal.

Assume HzU: z ∈ U.

An exact proof term for the current goal is HzU.

Assume HznotU: z ∉ U.

We prove the intermediate claim HzB: z ∈ B.

An exact proof term for the current goal is (setminusI X U z HzX HznotU).

We prove the intermediate claim HzW0: z ∈ W0.

An exact proof term for the current goal is (HBsubW0 z HzB).

We prove the intermediate claim Hcliff: z ∈ closure_of X Tx V0 ↔ (∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty).

An exact proof term for the current goal is (closure_characterization X Tx V0 z HTx HzX).

We prove the intermediate claim Hneigh: ∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty.

An exact proof term for the current goal is (iffEL (z ∈ closure_of X Tx V0) (∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty) Hcliff Hzcl).

We prove the intermediate claim Hcontr: W0 ∩ V0 ≠ Empty.

An exact proof term for the current goal is (Hneigh W0 HW0Tx HzW0).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hcontr HdisjWV).

We use V0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV0Tx.

An exact proof term for the current goal is HxV0.

An exact proof term for the current goal is HclV0subU.

Assume Hcrit: ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U.

We will prove regular_space X Tx.

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.

Set U0 to be the term X ∖ F.

We prove the intermediate claim Hop0: open_in X Tx U0.

An exact proof term for the current goal is (open_of_closed_complement X Tx F HFcl).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andER (topology_on X Tx) (U0 ∈ Tx) Hop0).

We prove the intermediate claim HxU0: x ∈ U0.

An exact proof term for the current goal is (setminusI X F x HxX HxnotF).

We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U0.

An exact proof term for the current goal is (Hcrit x U0 HxX HU0Tx HxU0).

Set V0 to be the term Eps_i (λV : set ⇒ V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U0).

We prove the intermediate claim HV0prop: V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U0) HexV).

We prove the intermediate claim HV0TxHx: V0 ∈ Tx ∧ x ∈ V0.

An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0prop).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

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

We prove the intermediate claim HxV0: x ∈ V0.

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

We prove the intermediate claim Hclsub: closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0prop).

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 HV0subX: V0 ⊆ X.

An exact proof term for the current goal is (PowerE X V0 (HTsub V0 HV0Tx)).

We prove the intermediate claim HclV0cl: closed_in X Tx (closure_of X Tx V0).

An exact proof term for the current goal is (closure_is_closed X Tx V0 HTx HV0subX).

Set W0 to be the term X ∖ closure_of X Tx V0.

We prove the intermediate claim HopW: open_in X Tx W0.

An exact proof term for the current goal is (open_of_closed_complement X Tx (closure_of X Tx V0) HclV0cl).

We prove the intermediate claim HW0Tx: W0 ∈ Tx.

An exact proof term for the current goal is (andER (topology_on X Tx) (W0 ∈ Tx) HopW).

We prove the intermediate claim HFsubW0: F ⊆ W0.

Let z be given.

Assume HzF: z ∈ F.

We will prove z ∈ W0.

We prove the intermediate claim HFsubX: F ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (HFsubX z HzF).

Apply xm (z ∈ closure_of X Tx V0) to the current goal.

Assume Hzcl: z ∈ closure_of X Tx V0.

We prove the intermediate claim HzU0: z ∈ U0.

An exact proof term for the current goal is (Hclsub z Hzcl).

We prove the intermediate claim HznotF2: z ∉ F.

An exact proof term for the current goal is (setminusE2 X F z HzU0).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HznotF2 HzF).

Assume Hznotcl: z ∉ closure_of X Tx V0.

An exact proof term for the current goal is (setminusI X (closure_of X Tx V0) z HzX Hznotcl).

We prove the intermediate claim HVsubcl: V0 ⊆ closure_of X Tx V0.

An exact proof term for the current goal is (subset_of_closure X Tx V0 HTx HV0subX).

We prove the intermediate claim Hdisj: V0 ∩ W0 = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ V0 ∩ W0.

We will prove z ∈ Empty.

We prove the intermediate claim HzV: z ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 W0 z Hz).

We prove the intermediate claim HzW: z ∈ W0.

An exact proof term for the current goal is (binintersectE2 V0 W0 z Hz).

We prove the intermediate claim Hzcl: z ∈ closure_of X Tx V0.

An exact proof term for the current goal is (HVsubcl z HzV).

We prove the intermediate claim Hznotcl: z ∉ closure_of X Tx V0.

An exact proof term for the current goal is (setminusE2 X (closure_of X Tx V0) z HzW).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hznotcl Hzcl).

We use V0 to witness the existential quantifier.

We use W0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV0Tx.

An exact proof term for the current goal is HW0Tx.

An exact proof term for the current goal is HxV0.

An exact proof term for the current goal is HFsubW0.

An exact proof term for the current goal is Hdisj.

Assume HT1: one_point_sets_closed X Tx.

We will prove normal_space X Tx ↔ ∀A U : set, closed_in X Tx A → U ∈ Tx → A ⊆ U → ∃V : set, V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U.

Apply iffI to the current goal.

Assume Hnorm: normal_space X Tx.

We will prove ∀A U : set, closed_in X Tx A → U ∈ Tx → A ⊆ U → ∃V : set, V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U.

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).

Let A and U be given.

Assume HAcl: closed_in X Tx A.

Assume HU: U ∈ Tx.

Assume HAsubU: A ⊆ U.

Set B to be the term X ∖ U.

We prove the intermediate claim HBcl: closed_in X Tx B.

An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HU).

We prove the intermediate claim HABdisj: A ∩ B = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ A ∩ B.

We will prove z ∈ Empty.

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE1 A B z Hz).

We prove the intermediate claim HzB: z ∈ B.

An exact proof term for the current goal is (binintersectE2 A B z Hz).

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (HAsubU z HzA).

We prove the intermediate claim HznotU: z ∉ U.

An exact proof term for the current goal is (setminusE2 X U z HzB).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HznotU HzU).

We prove the intermediate claim Hex: ∃V W : set, V ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V ∧ B ⊆ W ∧ V ∩ W = Empty.

An exact proof term for the current goal is (HSepNorm A B HAcl HBcl HABdisj).

Set V0 to be the term Eps_i (λV : set ⇒ ∃W : set, V ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V ∧ B ⊆ W ∧ V ∩ W = Empty).

We prove the intermediate claim HV0ex: ∃W : set, V0 ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ ∃W : set, V ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V ∧ B ⊆ W ∧ V ∩ W = Empty) Hex).

Set W0 to be the term Eps_i (λW : set ⇒ V0 ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty).

We prove the intermediate claim HW0prop: V0 ∈ Tx ∧ W0 ∈ Tx ∧ A ⊆ V0 ∧ B ⊆ W0 ∧ V0 ∩ W0 = Empty.

An exact proof term for the current goal is (Eps_i_ex (λW : set ⇒ V0 ∈ Tx ∧ W ∈ Tx ∧ A ⊆ V0 ∧ B ⊆ W ∧ V0 ∩ W = Empty) HV0ex).

We prove the intermediate claim H1234: (((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0) ∧ B ⊆ W0).

An exact proof term for the current goal is (andEL ((((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0) ∧ B ⊆ W0)) (V0 ∩ W0 = Empty) HW0prop).

We prove the intermediate claim HdisjVW: V0 ∩ W0 = Empty.

An exact proof term for the current goal is (andER ((((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0) ∧ B ⊆ W0)) (V0 ∩ W0 = Empty) HW0prop).

We prove the intermediate claim H123: ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0).

An exact proof term for the current goal is (andEL ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0) (B ⊆ W0) H1234).

We prove the intermediate claim H12: (V0 ∈ Tx ∧ W0 ∈ Tx).

An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ W0 ∈ Tx) (A ⊆ V0) H123).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

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

We prove the intermediate claim HW0Tx: W0 ∈ Tx.

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

We prove the intermediate claim HAsubV0: A ⊆ V0.

An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ W0 ∈ Tx) (A ⊆ V0) H123).

We prove the intermediate claim HBsubW0: B ⊆ W0.

An exact proof term for the current goal is (andER ((V0 ∈ Tx ∧ W0 ∈ Tx) ∧ A ⊆ V0) (B ⊆ W0) H1234).

We prove the intermediate claim HdisjWV: W0 ∩ V0 = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ W0 ∩ V0.

We will prove z ∈ Empty.

We prove the intermediate claim HzW: z ∈ W0.

An exact proof term for the current goal is (binintersectE1 W0 V0 z Hz).

We prove the intermediate claim HzV: z ∈ V0.

An exact proof term for the current goal is (binintersectE2 W0 V0 z Hz).

We prove the intermediate claim HzVW: z ∈ V0 ∩ W0.

An exact proof term for the current goal is (binintersectI V0 W0 z HzV HzW).

We prove the intermediate claim HzE: z ∈ Empty.

rewrite the current goal using HdisjVW (from right to left).

An exact proof term for the current goal is HzVW.

An exact proof term for the current goal is HzE.

We prove the intermediate claim HclV0subU: closure_of X Tx V0 ⊆ U.

Let z be given.

Assume Hzcl: z ∈ closure_of X Tx V0.

We will prove z ∈ U.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀N : set, N ∈ Tx → z0 ∈ N → N ∩ V0 ≠ Empty) z Hzcl).

Apply xm (z ∈ U) to the current goal.

Assume HzU: z ∈ U.

An exact proof term for the current goal is HzU.

Assume HznotU: z ∉ U.

We prove the intermediate claim HzB: z ∈ B.

An exact proof term for the current goal is (setminusI X U z HzX HznotU).

We prove the intermediate claim HzW0: z ∈ W0.

An exact proof term for the current goal is (HBsubW0 z HzB).

We prove the intermediate claim Hcliff: z ∈ closure_of X Tx V0 ↔ (∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty).

An exact proof term for the current goal is (closure_characterization X Tx V0 z HTx HzX).

We prove the intermediate claim Hneigh: ∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty.

An exact proof term for the current goal is (iffEL (z ∈ closure_of X Tx V0) (∀N ∈ Tx, z ∈ N → N ∩ V0 ≠ Empty) Hcliff Hzcl).

We prove the intermediate claim Hcontr: W0 ∩ V0 ≠ Empty.

An exact proof term for the current goal is (Hneigh W0 HW0Tx HzW0).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hcontr HdisjWV).

We use V0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV0Tx.

An exact proof term for the current goal is HAsubV0.

An exact proof term for the current goal is HclV0subU.

Assume Hcrit: ∀A U : set, closed_in X Tx A → U ∈ Tx → A ⊆ U → ∃V : set, V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U.

We will prove normal_space X Tx.

We will prove 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.

Apply andI to the current goal.

An exact proof term for the current goal is HT1.

Let A be given.

Let B be given.

Assume HAcl: closed_in X Tx A.

Assume HBcl: closed_in X Tx B.

Assume Hdisj: A ∩ B = Empty.

We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.

Set U0 to be the term X ∖ B.

We prove the intermediate claim Hop0: open_in X Tx U0.

An exact proof term for the current goal is (open_of_closed_complement X Tx B HBcl).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andER (topology_on X Tx) (U0 ∈ Tx) Hop0).

We prove the intermediate claim HAsubU0: A ⊆ U0.

Let z be given.

Assume HzA: z ∈ A.

We will prove z ∈ U0.

We prove the intermediate claim HAsubX: A ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (HAsubX z HzA).

Apply xm (z ∈ B) to the current goal.

Assume HzB: z ∈ B.

We prove the intermediate claim HzAB: z ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B z HzA HzB).

We prove the intermediate claim HzE: z ∈ Empty.

rewrite the current goal using Hdisj (from right to left).

An exact proof term for the current goal is HzAB.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE z HzE False).

Assume HznotB: z ∉ B.

An exact proof term for the current goal is (setminusI X B z HzX HznotB).

We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U0.

An exact proof term for the current goal is (Hcrit A U0 HAcl HU0Tx HAsubU0).

Set V0 to be the term Eps_i (λV : set ⇒ V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U0).

We prove the intermediate claim HV0prop: V0 ∈ Tx ∧ A ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Tx ∧ A ⊆ V ∧ closure_of X Tx V ⊆ U0) HexV).

We prove the intermediate claim HV0TxHA: V0 ∈ Tx ∧ A ⊆ V0.

An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ A ⊆ V0) (closure_of X Tx V0 ⊆ U0) HV0prop).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

An exact proof term for the current goal is (andEL (V0 ∈ Tx) (A ⊆ V0) HV0TxHA).

We prove the intermediate claim HAsubV0: A ⊆ V0.

An exact proof term for the current goal is (andER (V0 ∈ Tx) (A ⊆ V0) HV0TxHA).

We prove the intermediate claim Hclsub: closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ A ⊆ V0) (closure_of X Tx V0 ⊆ U0) HV0prop).

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 HV0subX: V0 ⊆ X.

An exact proof term for the current goal is (PowerE X V0 (HTsub V0 HV0Tx)).

We prove the intermediate claim HclV0cl: closed_in X Tx (closure_of X Tx V0).

An exact proof term for the current goal is (closure_is_closed X Tx V0 HTx HV0subX).

Set W0 to be the term X ∖ closure_of X Tx V0.

We prove the intermediate claim HopW: open_in X Tx W0.

An exact proof term for the current goal is (open_of_closed_complement X Tx (closure_of X Tx V0) HclV0cl).

We prove the intermediate claim HW0Tx: W0 ∈ Tx.

An exact proof term for the current goal is (andER (topology_on X Tx) (W0 ∈ Tx) HopW).

We prove the intermediate claim HBsubW0: B ⊆ W0.

Let z be given.

Assume HzB: z ∈ B.

We will prove z ∈ W0.

We prove the intermediate claim HBsubX: B ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx B HBcl).

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (HBsubX z HzB).

Apply xm (z ∈ closure_of X Tx V0) to the current goal.

Assume Hzcl: z ∈ closure_of X Tx V0.

We prove the intermediate claim HzU0: z ∈ U0.

An exact proof term for the current goal is (Hclsub z Hzcl).

We prove the intermediate claim HznotB: z ∉ B.

An exact proof term for the current goal is (setminusE2 X B z HzU0).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HznotB HzB).

Assume Hznotcl: z ∉ closure_of X Tx V0.

An exact proof term for the current goal is (setminusI X (closure_of X Tx V0) z HzX Hznotcl).

We prove the intermediate claim HVsubcl: V0 ⊆ closure_of X Tx V0.

An exact proof term for the current goal is (subset_of_closure X Tx V0 HTx HV0subX).

We prove the intermediate claim HdisjVW: V0 ∩ W0 = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ V0 ∩ W0.

We will prove z ∈ Empty.

We prove the intermediate claim HzV: z ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 W0 z Hz).

We prove the intermediate claim HzW: z ∈ W0.

An exact proof term for the current goal is (binintersectE2 V0 W0 z Hz).

We prove the intermediate claim Hzcl: z ∈ closure_of X Tx V0.

An exact proof term for the current goal is (HVsubcl z HzV).

We prove the intermediate claim Hznotcl: z ∉ closure_of X Tx V0.

An exact proof term for the current goal is (setminusE2 X (closure_of X Tx V0) z HzW).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hznotcl Hzcl).

We use V0 to witness the existential quantifier.

We use W0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV0Tx.

An exact proof term for the current goal is HW0Tx.

An exact proof term for the current goal is HAsubV0.

An exact proof term for the current goal is HBsubW0.

An exact proof term for the current goal is HdisjVW.