Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim Hcl: ∀U : set, U ∈ finite_complement_topology X → x ∈ U → U ∩ A ≠ Empty.

Let U be given.

Assume HxU: x ∈ U.

We will prove U ∩ A ≠ Empty.

We prove the intermediate claim HUne: U ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty U x HxU).

We prove the intermediate claim HUcases: finite (X ∖ U) ∨ U = Empty.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU).

We prove the intermediate claim HfinComp: finite (X ∖ U).

Apply (HUcases (finite (X ∖ U))) to the current goal.

Assume Hfin.

An exact proof term for the current goal is Hfin.

Assume HUe.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HUne HUe).

Assume Hempty: U ∩ A = Empty.

We prove the intermediate claim Hsub: A ⊆ X ∖ U.

Let a be given.

Assume HaA: a ∈ A.

We will prove a ∈ X ∖ U.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (HAsub a HaA).

We prove the intermediate claim HanotU: a ∉ U.

Assume HaU: a ∈ U.

We prove the intermediate claim HaUA: a ∈ U ∩ A.

An exact proof term for the current goal is (binintersectI U A a HaU HaA).

We prove the intermediate claim HaE: a ∈ Empty.

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

An exact proof term for the current goal is HaUA.

An exact proof term for the current goal is (EmptyE a HaE).

An exact proof term for the current goal is (setminusI X U a HaX HanotU).

We prove the intermediate claim HfinA: finite A.

An exact proof term for the current goal is (Subq_finite (X ∖ U) HfinComp A Hsub).

An exact proof term for the current goal is (HinfA HfinA).

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ finite_complement_topology X → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hcl).