Let X, Tx and A be given.
Assume HTx: topology_on X Tx.
We will prove locally_finite_family X Tx {A}.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ {A} ∧ ∀B : set, B ∈ {A} → B ∩ N ≠ Empty → B ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We use X to witness the existential quantifier.
We will prove X ∈ Tx ∧ x ∈ X ∧ ∃S : set, finite S ∧ S ⊆ {A} ∧ ∀B : set, B ∈ {A} → B ∩ X ≠ Empty → B ∈ S.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
An exact proof term for the current goal is HxX.
We use {A} to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (Sing_finite A).
An exact proof term for the current goal is (Subq_ref {A}).
Let B be given.
Assume HB: B ∈ {A}.
Assume _: B ∩ X ≠ Empty.
We will prove B ∈ {A}.
An exact proof term for the current goal is HB.
∎