Let X and U be given.

Assume Hopen.

We prove the intermediate claim HUin: U ∈ finite_complement_topology X.

An exact proof term for the current goal is (andER (topology_on X (finite_complement_topology X)) (U ∈ finite_complement_topology X) Hopen).

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

∎