Let X and T be given.

Assume HTx: topology_on X T.

We will prove open_in X T Empty.

We will prove topology_on X T ∧ Empty ∈ 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_empty X T HTx).

∎