Let X, T, U and V be given.
Assume HTx: topology_on X T.
Assume HU: U ∈ T.
Assume HV: V ∈ T.
We will prove U ∩ V ∈ T.
We prove the intermediate claim HIntersectAxiom: ∀U0 ∈ T, ∀V0 ∈ T, U0 ∩ V0 ∈ T.
An exact proof term for the current goal is (andER ((((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T))) (∀U0 ∈ T, ∀V0 ∈ T, U0 ∩ V0 ∈ T) HTx).
An exact proof term for the current goal is (HIntersectAxiom U HU V HV).
∎