Let X be given.
We will prove finite_complement_topology X ⊆ discrete_topology X.
Let U be given.
Assume HU.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU).
∎