Let X, Tx, phi and U be given.

Assume HTx: topology_on X Tx.

Assume HUsubX: U ⊆ X.

Assume HnzSub: ∀x : set, x ∈ X → apply_fun phi x ≠ 0 → x ∈ U.

We will prove support_of X Tx phi ⊆ closure_of X Tx U.

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

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

We prove the intermediate claim HnzsubU: nz ⊆ U.

Let x be given.

Assume Hx: x ∈ nz.

We prove the intermediate claim HxX: x ∈ X.

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

We prove the intermediate claim Hxneq: apply_fun phi x ≠ 0.

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

An exact proof term for the current goal is (HnzSub x HxX Hxneq).

An exact proof term for the current goal is (closure_monotone X Tx nz U HTx HnzsubU HUsubX).

∎