Let X and T be given.
Assume HTx: topology_on X T.
We will prove closed_in X T Empty.
Apply (closed_inI X T Empty) to the current goal.
An exact proof term for the current goal is HTx.
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 T HTx).
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).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotX HxX).
∎