Let X and T be given.

Assume HTx: topology_on X T.

We will prove T ⊆ 𝒫 X.

We prove the intermediate claim H0: ((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) HTx).

We prove the intermediate claim H1: (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) H0).

We prove the intermediate claim H2: T ⊆ 𝒫 X ∧ Empty ∈ T.

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

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

∎