An exact proof term for the current goal is (andEL (B ⊆ 𝒫 X) (∀x ∈ X, ∃b ∈ B, x ∈ b) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ B, x ∈ b)) (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBasis)).

An exact proof term for the current goal is (andER (B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ B, x ∈ b)) (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBasis).

An exact proof term for the current goal is (PowerE X b0 (HBsub b0 Hb0)).

Let x be given.

Assume Hxb0.

We prove the intermediate claim Hexb3: ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b0 ∩ b0.

An exact proof term for the current goal is (HBint b0 Hb0 b0 Hb0 x Hxb0 Hxb0).

Apply Hexb3 to the current goal.

Let b3 be given.

Assume Hb3pair.

We prove the intermediate claim Hb3: b3 ∈ B.

An exact proof term for the current goal is (andEL (b3 ∈ B) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0) Hb3pair).

We prove the intermediate claim Hb3prop: x ∈ b3 ∧ b3 ⊆ b0 ∩ b0.

An exact proof term for the current goal is (andER (b3 ∈ B) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0) Hb3pair).

We prove the intermediate claim Hxb3: x ∈ b3.

An exact proof term for the current goal is (andEL (x ∈ b3) (b3 ⊆ b0 ∩ b0) Hb3prop).

We prove the intermediate claim Hb3sub_inter: b3 ⊆ b0 ∩ b0.

An exact proof term for the current goal is (andER (x ∈ b3) (b3 ⊆ b0 ∩ b0) Hb3prop).

We prove the intermediate claim Hb3subb0: b3 ⊆ b0.

Let y be given.

Assume Hyb3.

We prove the intermediate claim Hycap: y ∈ b0 ∩ b0.

An exact proof term for the current goal is (Hb3sub_inter y Hyb3).

Apply binintersectE b0 b0 y Hycap to the current goal.

Assume Hy1 Hy2.

An exact proof term for the current goal is Hy1.

We use b3 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hb3.

Apply andI to the current goal.

An exact proof term for the current goal is Hxb3.

An exact proof term for the current goal is Hb3subb0.