Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove locally_finite_family X Tx Empty.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Empty ∧ ∀A : set, A ∈ Empty → A ∩ N ≠ Empty → A ∈ 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.
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 Empty 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 finite_Empty.
An exact proof term for the current goal is (Subq_Empty Empty).
Let A be given.
Assume HA: A ∈ Empty.
Assume _: A ∩ X ≠ Empty.
We will prove A ∈ Empty.
An exact proof term for the current goal is HA.
∎