Let X and Tx be given.

Assume Htop: topology_on X Tx.

We will prove interior_of X Tx X = X.

We prove the intermediate claim HXopen: X ∈ Tx.

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

An exact proof term for the current goal is (open_interior_eq X Tx X Htop HXopen).

∎