Let X, S and s be given.
Assume HSsub HsS HsNonempty.
We will prove s ∈ basis_of_subbasis X S.
We prove the intermediate claim HS: S ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (S ⊆ 𝒫 X) (⋃ S = X) HSsub).
We prove the intermediate claim HsPow: s ∈ 𝒫 X.
An exact proof term for the current goal is (HS s HsS).
We prove the intermediate claim HsSubX: s ⊆ X.
An exact proof term for the current goal is (PowerE X s HsPow).
Set F to be the term {s}.
We prove the intermediate claim HFPower: F ∈ 𝒫 S.
Apply PowerI S F to the current goal.
Let t be given.
Assume Ht: t ∈ F.
We will prove t ∈ S.
We prove the intermediate claim HtEq: t = s.
An exact proof term for the current goal is (SingE s t Ht).
rewrite the current goal using HtEq (from left to right).
An exact proof term for the current goal is HsS.
We prove the intermediate claim HFinF: finite F.
An exact proof term for the current goal is (Sing_finite s).
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 = s.
An exact proof term for the current goal is (intersection_of_family_singleton_eq X s HsSubX).
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 HsNonempty.
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.
∎