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