Let X, S and b be given.
Assume Hb: b ∈ basis_of_subbasis X S.
We will prove ∃F : set, F ∈ finite_subcollections S ∧ b = intersection_of_family X F ∧ b ≠ Empty.
We prove the intermediate claim HbFin: b ∈ finite_intersections_of X S.
An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) b Hb).
We prove the intermediate claim HbNe: b ≠ Empty.
An exact proof term for the current goal is (SepE2 (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) b Hb).
We prove the intermediate claim HexF: ∃F ∈ finite_subcollections S, b = intersection_of_family X F.
An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) b HbFin).
Apply HexF to the current goal.
Let F be given.
Assume HFand.
We use F to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (b = intersection_of_family X F) HFand).
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (b = intersection_of_family X F) HFand).
An exact proof term for the current goal is HbNe.
∎