Let X, Tx and F be given.

Let x be given.

Assume HxX: x ∈ X.

We will prove ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → x ∈ A → A ∈ S.

We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HLF x HxX).

Apply HexN to the current goal.

Let N be given.

Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.

We prove the intermediate claim HNpair: N ∈ Tx ∧ x ∈ N.

An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HN).

We prove the intermediate claim HxN: x ∈ N.

An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNpair).

We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HN).

Apply HexS to the current goal.

Let S be given.

Assume HS: finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.

We use S to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ F) (∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HS).

Let A be given.

Assume HA: A ∈ F.

Assume HxA: x ∈ A.

We prove the intermediate claim HxAN: x ∈ A ∩ N.

An exact proof term for the current goal is (binintersectI A N x HxA HxN).

We prove the intermediate claim HAnN: A ∩ N ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty (A ∩ N) x HxAN).

An exact proof term for the current goal is (andER (finite S ∧ S ⊆ F) (∀A0 : set, A0 ∈ F → A0 ∩ N ≠ Empty → A0 ∈ S) HS A HA HAnN).

∎