Let X, Tx, P, x, N and F0 be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
Assume HNTx: N ∈ Tx.
Assume HxN: x ∈ N.
Assume HF0fin: finite F0.
Assume HF0sub: F0 ⊆ P.
Assume Hctrl: ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
Let f be given.
Assume HfP: f ∈ P.
Assume Hfx: apply_fun f x ≠ 0.
We will prove f ∈ F0.
We prove the intermediate claim HxSupp: x ∈ support_of X Tx f.
An exact proof term for the current goal is (support_of_contains_nonzero X Tx f x HTx HxX Hfx).
We prove the intermediate claim HSuppMeet: support_of X Tx f ∩ N ≠ Empty.
Assume Hempty: support_of X Tx f ∩ N = Empty.
We prove the intermediate claim HxInt: x ∈ support_of X Tx f ∩ N.
An exact proof term for the current goal is (binintersectI (support_of X Tx f) N x HxSupp HxN).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (EmptyE x HxE).
An exact proof term for the current goal is (Hctrl f HfP HSuppMeet).
∎