Let X, T and U be given.

Assume HT: topology_on X T.

Assume HU: U ∈ T.

An exact proof term for the current goal is (andI (topology_on X T) (U ∈ T) HT HU).

∎