Let X and T be given.

Assume HT.

An exact proof term for the current goal is (topology_sub_Power X T HT).

∎