Let X, T, C and D be given.

Assume HC: closed_in X T C.

Assume HD: closed_in X T D.

An exact proof term for the current goal is (closed_binintersect X T C D HC HD).

∎