Let X, Tx and phi be given.

Assume HTx: topology_on X Tx.

We will prove support_of X Tx phi ⊆ X.

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).

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

∎