Let X, Tx, f and g be given.

Assume HTx: topology_on X Tx.

Assume Hnz: ∀x : set, x ∈ X → apply_fun g x ≠ 0 → apply_fun f x ≠ 0.

We will prove support_of X Tx g ⊆ support_of X Tx f.

Set Ag to be the term {x ∈ X|apply_fun g x ≠ 0}.

Set Af to be the term {x ∈ X|apply_fun f x ≠ 0}.

We prove the intermediate claim HAgSubAf: Ag ⊆ Af.

Let x be given.

Assume Hx: x ∈ Ag.

We prove the intermediate claim HxX: x ∈ X.

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

We prove the intermediate claim Hgx: apply_fun g x ≠ 0.

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

Apply (SepI X (λz : set ⇒ apply_fun f z ≠ 0) x HxX) to the current goal.

An exact proof term for the current goal is (Hnz x HxX Hgx).

We prove the intermediate claim HAfSubX: Af ⊆ X.

An exact proof term for the current goal is (Sep_Subq X (λz : set ⇒ apply_fun f z ≠ 0)).

We prove the intermediate claim HclMon: closure_of X Tx Ag ⊆ closure_of X Tx Af.

An exact proof term for the current goal is (closure_monotone X Tx Ag Af HTx HAgSubAf HAfSubX).

An exact proof term for the current goal is HclMon.

∎