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

Let x1 and x2 be given.

Assume Hx1: x1 ∈ X.

Assume Hx2: x2 ∈ X.

Assume Hne: x1 ≠ x2.

Apply (Hsep x1 x2 Hx1 Hx2 Hne) to the current goal.

Let U be given.

Assume HexV.

Apply HexV to the current goal.

Let V be given.

Assume HUV.

We use U to witness the existential quantifier.

We use V to witness the existential quantifier.

We prove the intermediate claim Hpre: (((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V).

An exact proof term for the current goal is (andEL (((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V) (U ∩ V = Empty) HUV).

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

An exact proof term for the current goal is (andER (((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V) (U ∩ V = Empty) HUV).

We prove the intermediate claim Hpre2: ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U).

An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) (x2 ∈ V) Hpre).

We prove the intermediate claim Hx2V: x2 ∈ V.

An exact proof term for the current goal is (andER ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) (x2 ∈ V) Hpre).

We prove the intermediate claim Hpair: (U ∈ Tx ∧ V ∈ Tx).

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ V ∈ Tx) (x1 ∈ U) Hpre2).

We prove the intermediate claim Hx1U: x1 ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (x1 ∈ U) Hpre2).

We prove the intermediate claim HUinTx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) Hpair).

We prove the intermediate claim HVinTx: V ∈ Tx.

An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) Hpair).

We prove the intermediate claim HUinTy: U ∈ Ty.

An exact proof term for the current goal is (Hsub U HUinTx).

We prove the intermediate claim HVinTy: V ∈ Ty.

An exact proof term for the current goal is (Hsub V HVinTx).

We will prove U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

Apply andI to the current goal.

We will prove ((U ∈ Ty ∧ V ∈ Ty) ∧ x1 ∈ U) ∧ x2 ∈ V.

Apply andI to the current goal.

We will prove (U ∈ Ty ∧ V ∈ Ty) ∧ x1 ∈ U.

Apply andI to the current goal.

We will prove U ∈ Ty ∧ V ∈ Ty.

Apply andI to the current goal.

An exact proof term for the current goal is HUinTy.

An exact proof term for the current goal is HVinTy.

An exact proof term for the current goal is Hx1U.

An exact proof term for the current goal is Hx2V.

An exact proof term for the current goal is Hempty.