Let X and S be given.

Assume HXnonempty.

We will prove X ∈ basis_of_subbasis X S.

Set F to be the term Empty.

We prove the intermediate claim HFPower: F ∈ 𝒫 S.

An exact proof term for the current goal is (Empty_In_Power S).

We prove the intermediate claim HFinF: finite F.

An exact proof term for the current goal is finite_Empty.

We prove the intermediate claim HFsubcol: F ∈ finite_subcollections S.

An exact proof term for the current goal is (SepI (𝒫 S) (λF0 : set ⇒ finite F0) F HFPower HFinF).

We prove the intermediate claim HinterEq: intersection_of_family X F = X.

An exact proof term for the current goal is (intersection_of_family_empty_eq X).

We prove the intermediate claim HinterNonempty: intersection_of_family X F ≠ Empty.

rewrite the current goal using HinterEq (from left to right).

An exact proof term for the current goal is HXnonempty.

We prove the intermediate claim HinterInBasis: intersection_of_family X F ∈ basis_of_subbasis X S.

An exact proof term for the current goal is (finite_intersection_in_basis X S F HFsubcol HinterNonempty).

rewrite the current goal using HinterEq (from right to left) at position 1.

An exact proof term for the current goal is HinterInBasis.

∎