Let X and T be given.

Assume HTx: topology_on X T.

We will prove ∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T.

Let U be given.

Assume HU: U ∈ T.

Let V be given.

Assume HV: V ∈ T.

An exact proof term for the current goal is (topology_binintersect_closed X T U V HTx HU HV).

∎