Let X, B and b be given.

Assume HB: basis_on X B.

Assume Hb: b ∈ B.

We will prove b ∈ generated_topology X B.

We prove the intermediate claim HbPower: b ∈ 𝒫 X.

We prove the intermediate claim HbsubX: b ⊆ X.

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

An exact proof term for the current goal is (PowerI X b HbsubX).

We prove the intermediate claim HbCond: ∀x ∈ b, ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ b.

Let x be given.

Assume Hx: x ∈ b.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hb.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

Apply Subq_ref to the current goal.

An exact proof term for the current goal is (SepI (𝒫 X) (λU ⇒ ∀x ∈ U, ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ U) b HbPower HbCond).

∎