Let X, Tx and phi be given.

Assume HTx: topology_on X Tx.

We will prove closed_in X Tx (support_of X Tx phi).

We prove the intermediate claim Hdef: support_of X Tx phi = closure_of X Tx {x ∈ X|apply_fun phi x ≠ 0}.

Use reflexivity.

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

We prove the intermediate claim Hsub: {x ∈ X|apply_fun phi x ≠ 0} ⊆ X.

Let x be given.

Assume Hx: x ∈ {x0 ∈ X|apply_fun phi x0 ≠ 0}.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun phi x0 ≠ 0) x Hx).

An exact proof term for the current goal is (closure_is_closed X Tx {x ∈ X|apply_fun phi x ≠ 0} HTx Hsub).

∎