Let y1 and y2 be given.

Assume Hy1: y1 ∈ Y.

Assume Hy2: y2 ∈ Y.

Assume Hne: y1 ≠ y2.

We will prove ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty.

We prove the intermediate claim Hsepax: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

Let x1 and x2 be given.

Assume Hx1: x1 ∈ X.

Assume Hx2: x2 ∈ X.

Assume Hneq: x1 ≠ x2.

An exact proof term for the current goal is (Hausdorff_space_separation X Tx x1 x2 HX Hx1 Hx2 Hneq).

We prove the intermediate claim Hy1X: y1 ∈ X.

An exact proof term for the current goal is (HYsubX y1 Hy1).

We prove the intermediate claim Hy2X: y2 ∈ X.

An exact proof term for the current goal is (HYsubX y2 Hy2).

We prove the intermediate claim HexistsUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (Hsepax y1 y2 Hy1X Hy2X Hne).

Set U0 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty).

We prove the intermediate claim HU0ex: ∃V : set, U0 ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U0 ∧ y2 ∈ V ∧ U0 ∩ V = Empty.

An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty) HexistsUV).

Set V0 to be the term Eps_i (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U0 ∧ y2 ∈ V ∧ U0 ∩ V = Empty).

We prove the intermediate claim HV0prop: U0 ∈ Tx ∧ V0 ∈ Tx ∧ y1 ∈ U0 ∧ y2 ∈ V0 ∧ U0 ∩ V0 = Empty.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ y1 ∈ U0 ∧ y2 ∈ V ∧ U0 ∩ V = Empty) HU0ex).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (y1 ∈ U0) (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) (y2 ∈ V0) (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) ∧ y2 ∈ V0) (U0 ∩ V0 = Empty) HV0prop)))).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (y1 ∈ U0) (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) (y2 ∈ V0) (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) ∧ y2 ∈ V0) (U0 ∩ V0 = Empty) HV0prop)))).

We prove the intermediate claim Hy1U0: y1 ∈ U0.

An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (y1 ∈ U0) (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) (y2 ∈ V0) (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) ∧ y2 ∈ V0) (U0 ∩ V0 = Empty) HV0prop))).

We prove the intermediate claim Hy2V0: y2 ∈ V0.

An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) (y2 ∈ V0) (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) ∧ y2 ∈ V0) (U0 ∩ V0 = Empty) HV0prop)).

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

An exact proof term for the current goal is (andER (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ y1 ∈ U0) ∧ y2 ∈ V0) (U0 ∩ V0 = Empty) HV0prop).

Set U to be the term U0 ∩ Y.

Set V to be the term V0 ∩ Y.

We prove the intermediate claim HUinST: U ∈ subspace_topology X Tx Y.

We prove the intermediate claim HUPowY: U ∈ 𝒫 Y.

Apply PowerI to the current goal.

Let z be given.

Assume Hz: z ∈ U.

An exact proof term for the current goal is (binintersectE2 U0 Y z Hz).

We prove the intermediate claim HUdef: ∃V' ∈ Tx, U = V' ∩ Y.

We use U0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU0Tx.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU1 : set ⇒ ∃V' ∈ Tx, U1 = V' ∩ Y) U HUPowY HUdef).

We prove the intermediate claim HVinST: V ∈ subspace_topology X Tx Y.

We prove the intermediate claim HVPowY: V ∈ 𝒫 Y.

Apply PowerI to the current goal.

Let z be given.

Assume Hz: z ∈ V.

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

We prove the intermediate claim HVdef: ∃V' ∈ Tx, V = V' ∩ Y.

We use V0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV0Tx.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU1 : set ⇒ ∃V' ∈ Tx, U1 = V' ∩ Y) V HVPowY HVdef).

We prove the intermediate claim Hy1U: y1 ∈ U.

An exact proof term for the current goal is (binintersectI U0 Y y1 Hy1U0 Hy1).

We prove the intermediate claim Hy2V: y2 ∈ V.

An exact proof term for the current goal is (binintersectI V0 Y y2 Hy2V0 Hy2).

We prove the intermediate claim HUVempty: U ∩ V = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U ∩ V.

We will prove z ∈ Empty.

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (binintersectE1 U V z Hz).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE2 U V z Hz).

We prove the intermediate claim HzU0: z ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 Y z HzU).

We prove the intermediate claim HzV0: z ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 Y z HzV).

We prove the intermediate claim HzU0V0: z ∈ U0 ∩ V0.

An exact proof term for the current goal is (binintersectI U0 V0 z HzU0 HzV0).

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

An exact proof term for the current goal is HzU0V0.

We use U to witness the existential quantifier.

We use V to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUinST.

An exact proof term for the current goal is HVinST.

An exact proof term for the current goal is Hy1U.

An exact proof term for the current goal is Hy2V.

An exact proof term for the current goal is HUVempty.