Let X and Tx be given.

Assume Htop: topology_on X Tx.

We will prove interior_of X Tx Empty = Empty.

Apply set_ext to the current goal.

An exact proof term for the current goal is (interior_subset X Tx Empty Htop).

An exact proof term for the current goal is (Subq_Empty (interior_of X Tx Empty)).

∎