Let X, Tx, phi and x be given.

Assume HTx: topology_on X Tx.

Assume HxX: x ∈ X.

Assume Hneq0: apply_fun phi x ≠ 0.

We will prove x ∈ support_of X Tx phi.

Set nz to be the term {y ∈ X|apply_fun phi y ≠ 0}.

We prove the intermediate claim HnzSubX: nz ⊆ X.

Let y be given.

Assume Hy: y ∈ nz.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ apply_fun phi y0 ≠ 0) y Hy).

We prove the intermediate claim HxNz: x ∈ nz.

An exact proof term for the current goal is (SepI X (λy0 : set ⇒ apply_fun phi y0 ≠ 0) x HxX Hneq0).

We prove the intermediate claim HxCl: x ∈ closure_of X Tx nz.

An exact proof term for the current goal is (subset_of_closure X Tx nz HTx HnzSubX x HxNz).

We prove the intermediate claim Hdef: support_of X Tx phi = closure_of X Tx nz.

Use reflexivity.

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

An exact proof term for the current goal is HxCl.

∎