Let X and Tx be given.
Assume Htop: topology_on X Tx.
We will prove closed_in X Tx Empty.
We will prove topology_on X Tx ∧ (Empty ⊆ X ∧ ∃U ∈ Tx, Empty = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
An exact proof term for the current goal is (Subq_Empty X).
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X Tx Htop).
We will prove Empty = X ∖ X.
Apply set_ext to the current goal.
An exact proof term for the current goal is (Subq_Empty (X ∖ X)).
Let x be given.
Assume Hx: x ∈ X ∖ X.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X X x Hx).
We prove the intermediate claim HxnotX: x ∉ X.
An exact proof term for the current goal is (setminusE2 X X x Hx).
We will prove x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotX HxX).
∎