Let X and T be given.

Assume HTx: topology_on X T.

We will prove X ∈ T.

We prove the intermediate claim H1: (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) ∧ (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T).

An exact proof term for the current goal is HTx.

We prove the intermediate claim H2: ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T).

An exact proof term for the current goal is (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) H1).

We prove the intermediate claim H3: (T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T.

An exact proof term for the current goal is (andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T) H2).

An exact proof term for the current goal is (andER (T ⊆ 𝒫 X ∧ Empty ∈ T) (X ∈ T) H3).

∎