Assume Hfiner.

Let x be given.

Assume HxX.

Let b be given.

Assume HbB Hxb.

We prove the intermediate claim HbGen: b ∈ generated_topology X B.

An exact proof term for the current goal is (generated_topology_contains_basis X B HB b HbB).

We prove the intermediate claim HbGen': b ∈ generated_topology X B'.

An exact proof term for the current goal is (Hfiner b HbGen).

We prove the intermediate claim Hbprop: ∀x0 ∈ b, ∃b' ∈ B', x0 ∈ b' ∧ b' ⊆ b.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B', x0 ∈ b0 ∧ b0 ⊆ U0) b HbGen').

An exact proof term for the current goal is (Hbprop x Hxb).