Let X, Tx and U be given.
Assume Htop: topology_on X Tx.
Assume HU: U ∈ Tx.
We will prove interior_of X Tx U = U.
Apply set_ext to the current goal.
An exact proof term for the current goal is (interior_subset X Tx U Htop).
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ interior_of X Tx U.
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x Hx).
We prove the intermediate claim Hwitness: U ∈ Tx ∧ x ∈ U ∧ U ⊆ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (Subq_ref U).
We prove the intermediate claim Hexists: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ U.
We use U to witness the existential quantifier.
An exact proof term for the current goal is Hwitness.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∃V : set, V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ U) x HxX Hexists).
∎