Let X and T be given.

Assume HTx: topology_on X T.

We will prove open_in X T X.

We will prove topology_on X T ∧ X ∈ T.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is (topology_has_X X T HTx).

∎