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