Let X, T and A be given.
Assume HT Hlocal.
We will prove open_in X T A.
Set Fam to be the term {U ∈ T|U ⊆ A} of type set.
We prove the intermediate claim HFam_sub: Fam ⊆ T.
Let U be given.
Assume HU.
An exact proof term for the current goal is (SepE1 T (λU0 ⇒ U0 ⊆ A) U HU).
We prove the intermediate claim HUnion_eq: ⋃ Fam = A.
Apply set_ext to the current goal.
Let x be given.
Assume Hx.
Apply UnionE_impred Fam x Hx to the current goal.
Let U be given.
Assume HxU HUFam.
We prove the intermediate claim HUsub: U ⊆ A.
An exact proof term for the current goal is (SepE2 T (λU0 ⇒ U0 ⊆ A) U HUFam).
An exact proof term for the current goal is (HUsub x HxU).
Let x be given.
Assume HxA.
We prove the intermediate claim Hex: ∃U ∈ T, x ∈ U ∧ U ⊆ A.
An exact proof term for the current goal is (Hlocal x HxA).
Apply Hex to the current goal.
Let U be given.
Assume HU.
We prove the intermediate claim HUT: U ∈ T.
An exact proof term for the current goal is (andEL (U ∈ T) (x ∈ U ∧ U ⊆ A) HU).
We prove the intermediate claim Hrest: x ∈ U ∧ U ⊆ A.
An exact proof term for the current goal is (andER (U ∈ T) (x ∈ U ∧ U ⊆ A) HU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ⊆ A) Hrest).
We prove the intermediate claim HUsub: U ⊆ A.
An exact proof term for the current goal is (andER (x ∈ U) (U ⊆ A) Hrest).
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (SepI T (λU0 ⇒ U0 ⊆ A) U HUT HUsub).
An exact proof term for the current goal is (UnionI Fam x U HxU HUFam).
We prove the intermediate claim HUnionT: ⋃ Fam ∈ T.
An exact proof term for the current goal is (topology_union_closed X T Fam HT HFam_sub).
We prove the intermediate claim HAT: A ∈ T.
rewrite the current goal using HUnion_eq (from right to left).
An exact proof term for the current goal is HUnionT.
We will prove topology_on X T ∧ A ∈ T.
Apply andI to the current goal.
An exact proof term for the current goal is HT.
An exact proof term for the current goal is HAT.
∎