Let X, Tx, Y and A be given.
Assume HY: closed_in X Tx Y.
Assume HA: closed_in Y (subspace_topology X Tx Y) A.
We will prove closed_in X Tx A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U) HY).
An exact proof term for the current goal is (closed_in_closed_subspace X Tx Y A HTx HY HA).
∎