Let X, Tx and A be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
We will prove interior_of X Tx A ∈ Tx.
Set F to be the term {U ∈ Tx|U ⊆ A}.
We prove the intermediate claim Hint_eq_union: interior_of X Tx A = ⋃ F.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ interior_of X Tx A.
We will prove x ∈ ⋃ F.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A) x Hx).
We prove the intermediate claim Hexists: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A) x Hx).
Apply Hexists to the current goal.
Let U be given.
Assume HU_conj: U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.
We prove the intermediate claim HU_and_x: U ∈ Tx ∧ x ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (U ⊆ A) HU_conj).
We prove the intermediate claim HUsub: U ⊆ A.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (U ⊆ A) HU_conj).
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HU_and_x).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HU_and_x).
We prove the intermediate claim HUinF: U ∈ F.
Apply SepI to the current goal.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is HUsub.
An exact proof term for the current goal is (UnionI F x U HxU HUinF).
Let x be given.
Assume Hx: x ∈ ⋃ F.
We will prove x ∈ interior_of X Tx A.
Apply (UnionE_impred F x Hx (x ∈ interior_of X Tx A)) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUinF: U ∈ F.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 ⇒ U0 ⊆ A) U HUinF).
We prove the intermediate claim HUsub: U ⊆ A.
An exact proof term for the current goal is (SepE2 Tx (λU0 ⇒ U0 ⊆ A) U HUinF).
We prove the intermediate claim HUsub_X: 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 x HxU).
We prove the intermediate claim Hwitness: U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.
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.
We prove the intermediate claim Hexists: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ A.
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 ⊆ A) x HxX Hexists).
We prove the intermediate claim HF_sub_Tx: F ⊆ Tx.
Let U be given.
Assume HU: U ∈ F.
An exact proof term for the current goal is (SepE1 Tx (λU0 ⇒ U0 ⊆ A) U HU).
We prove the intermediate claim Hunion_in_Tx: ⋃ F ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx F Htop HF_sub_Tx).
We prove the intermediate claim Heq_substitution: ∀S T : set, S = T → T ∈ Tx → S ∈ Tx.
Let S and T be given.
Assume HeqST: S = T.
Assume HTinTx: T ∈ Tx.
We will prove S ∈ Tx.
We prove the intermediate claim HST_equiv: ∀P : set → prop, P T → P S.
Let P be given.
Assume HPT: P T.
We will prove P S.
rewrite the current goal using HeqST (from left to right).
An exact proof term for the current goal is HPT.
An exact proof term for the current goal is (HST_equiv (λX0 ⇒ X0 ∈ Tx) HTinTx).
An exact proof term for the current goal is (Heq_substitution (interior_of X Tx A) (⋃ F) Hint_eq_union Hunion_in_Tx).
∎