Let X, Tx, A, U and x be given.
Assume HTx: topology_on X Tx.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
Assume HUsub: U ⊆ A.
We will prove x ∈ interior_of X Tx A.
We prove the intermediate claim HUsX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsX x HxU).
We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ⊆ 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 HU.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HUsub.
An exact proof term for the current goal is (SepI X (λy : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ y ∈ U0 ∧ U0 ⊆ A) x HxX Hex).
∎