Let X be given.
We will prove finite_complement_topology X ⊆ countable_complement_topology X.
Let U be given.
Assume HU: U ∈ finite_complement_topology X.
We prove the intermediate claim HUinPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU).
We prove the intermediate claim HUdata: 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 HUpred: countable (X ∖ U) ∨ U = Empty.
Apply HUdata (countable (X ∖ U) ∨ U = Empty) to the current goal.
Assume HUfin: finite (X ∖ U).
Apply orIL to the current goal.
An exact proof term for the current goal is (finite_countable (X ∖ U) HUfin).
Assume HUemp: U = Empty.
Apply orIR to the current goal.
An exact proof term for the current goal is HUemp.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ countable (X ∖ U0) ∨ U0 = Empty) U HUinPow HUpred).
∎