Let X, Tx, Y and U be given.

Assume HU: U ∈ subspace_topology X Tx Y.

Apply PowerI to the current goal.

An exact proof term for the current goal is (subspace_topology_subset X Tx Y U HU).

∎