Assume Hsep: ∃U V : set, U ∈ subspace_topology X Tx {x} ∧ V ∈ subspace_topology X Tx {x} ∧ separation_of {x} U V.

Apply Hsep to the current goal.

Let U be given.

Assume HexV: ∃V : set, U ∈ subspace_topology X Tx {x} ∧ V ∈ subspace_topology X Tx {x} ∧ separation_of {x} U V.

Apply HexV to the current goal.

Let V be given.

Assume HUV.

We prove the intermediate claim HopenUV: (U ∈ subspace_topology X Tx {x} ∧ V ∈ subspace_topology X Tx {x}) ∧ separation_of {x} U V.

An exact proof term for the current goal is HUV.

We prove the intermediate claim Hsepof: separation_of {x} U V.

An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx {x} ∧ V ∈ subspace_topology X Tx {x}) (separation_of {x} U V) HopenUV).

We prove the intermediate claim Hpre: ((((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).

An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = {x}) Hsepof).

We prove the intermediate claim Hpre2: (((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) ∧ U ≠ Empty).

An exact proof term for the current goal is (andEL (((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpre).

We prove the intermediate claim HUneq: U ≠ Empty.

An exact proof term for the current goal is (andER ((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) (U ≠ Empty) Hpre2).

We prove the intermediate claim HVneq: V ≠ Empty.

An exact proof term for the current goal is (andER ((((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) ∧ U ≠ Empty)) (V ≠ Empty) Hpre).

We prove the intermediate claim HpowDisj: (U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty.

An exact proof term for the current goal is (andEL ((U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) ∧ U ∩ V = Empty) (U ≠ Empty) Hpre2).

We prove the intermediate claim HpowUV: U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}.

An exact proof term for the current goal is (andEL (U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) (U ∩ V = Empty) HpowDisj).

We prove the intermediate claim HUpow: U ∈ 𝒫 {x}.

An exact proof term for the current goal is (andEL (U ∈ 𝒫 {x}) (V ∈ 𝒫 {x}) HpowUV).

We prove the intermediate claim HVpow: V ∈ 𝒫 {x}.

An exact proof term for the current goal is (andER (U ∈ 𝒫 {x}) (V ∈ 𝒫 {x}) HpowUV).

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

An exact proof term for the current goal is (andER (U ∈ 𝒫 {x} ∧ V ∈ 𝒫 {x}) (U ∩ V = Empty) HpowDisj).

Apply (nonempty_has_element U HUneq) to the current goal.

Let u be given.

Assume Hu: u ∈ U.

Apply (nonempty_has_element V HVneq) to the current goal.

Let v be given.

Assume Hv: v ∈ V.

We prove the intermediate claim HUsub: U ⊆ {x}.

An exact proof term for the current goal is (PowerE {x} U HUpow).

We prove the intermediate claim HVsub: V ⊆ {x}.

An exact proof term for the current goal is (PowerE {x} V HVpow).

We prove the intermediate claim Hux: u = x.

An exact proof term for the current goal is (SingE x u (HUsub u Hu)).

We prove the intermediate claim Hvx: v = x.

An exact proof term for the current goal is (SingE x v (HVsub v Hv)).

We prove the intermediate claim HxU: x ∈ U.

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

An exact proof term for the current goal is Hu.

We prove the intermediate claim HxV: x ∈ V.

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

An exact proof term for the current goal is Hv.

We prove the intermediate claim HxUV: x ∈ U ∩ V.

An exact proof term for the current goal is (binintersectI U V x HxU HxV).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxUV.

An exact proof term for the current goal is (EmptyE x HxE).