Let X, Tx and B be given.
Assume Hgen: basis_generates X B Tx.
We will prove basis_refines X B Tx.
We will prove topology_on X Tx ∧ (∀U ∈ Tx, ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U).
Apply andI to the current goal.
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) Hgen).
We prove the intermediate claim HtopGen: topology_on X (generated_topology X B).
An exact proof term for the current goal is (lemma_topology_from_basis X B HBasis).
We prove the intermediate claim Heq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) Hgen).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HtopGen.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim Heq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) Hgen).
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x1 ∈ U0, ∃b0 ∈ B, x1 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
An exact proof term for the current goal is (HUprop x HxU).
∎