Let X, T and U be given.

Assume H: open_in X T U.

An exact proof term for the current goal is (andEL (topology_on X T) (U ∈ T) H).

∎