Let X, T, T' and Y be given.

Assume Heq: T = T'.

We will prove subspace_topology X T Y = subspace_topology X T' Y.

rewrite the current goal using Heq (from left to right).

Use reflexivity.

∎