Assume HIne: I ≠ Empty.

Set X to be the term product_space I Xi.

Set Tx to be the term product_topology_full I Xi.

Set S to be the term product_subbasis_full I Xi.

We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hc: compact_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hcomp i HiI).

We prove the intermediate claim Htop: topology_on (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (compact_space_topology (product_component Xi i) (product_component_topology Xi i) Hc).

rewrite the current goal using (space_family_set_eq_product_component Xi i) (from left to right).

rewrite the current goal using (space_family_topology_eq_product_component_topology Xi i) (from left to right).

An exact proof term for the current goal is Htop.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (product_topology_full_is_topology I Xi HcompTop).

Apply (compact_space_of_closed_FIP_intersection_nonempty X Tx HTx) to the current goal.

Let A be given.

Assume HclosedA: ∀C : set, C ∈ A → closed_in X Tx C.

Assume HfipA: finite_intersection_property X A.

We will prove intersection_of_family X A ≠ Empty.

We prove the intermediate claim HexD: ∃D : set, A ⊆ D ∧ maximal_finite_intersection_property X D.

An exact proof term for the current goal is (Lemma37_1_maximal_fip_extension X A HfipA).

Apply HexD to the current goal.

Let D be given.

Assume HDpair.

We prove the intermediate claim HAsubD: A ⊆ D.

An exact proof term for the current goal is (andEL (A ⊆ D) (maximal_finite_intersection_property X D) HDpair).

We prove the intermediate claim HmaxD: maximal_finite_intersection_property X D.

An exact proof term for the current goal is (andER (A ⊆ D) (maximal_finite_intersection_property X D) HDpair).

We prove the intermediate claim HfipD: finite_intersection_property X D.

An exact proof term for the current goal is (andEL (finite_intersection_property X D) (∀E : set, D ⊆ E → finite_intersection_property X E → E ⊆ D) HmaxD).

We prove the intermediate claim HDpow: D ⊆ 𝒫 X.

An exact proof term for the current goal is (andEL (D ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ D → intersection_of_family X F ≠ Empty) HfipD).

We prove the intermediate claim HDfip: ∀F : set, finite F → F ⊆ D → intersection_of_family X F ≠ Empty.

An exact proof term for the current goal is (andER (D ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ D → intersection_of_family X F ≠ Empty) HfipD).

Set proj to be the term λi : set ⇒ λE : set ⇒ Repl E (λf : set ⇒ apply_fun (product_eval_map I Xi i) f).

Set closproj to be the term λi : set ⇒ λE : set ⇒ closure_of (space_family_set Xi i) (space_family_topology Xi i) (proj i E).

Set Dproj to be the term λi : set ⇒ {closproj i E|E ∈ D}.

We prove the intermediate claim HevFun: ∀i : set, i ∈ I → function_on (product_eval_map I Xi i) X (space_family_set Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hcont: continuous_map X Tx (space_family_set Xi i) (space_family_topology Xi i) (product_eval_map I Xi i).

An exact proof term for the current goal is (product_eval_map_continuous I Xi i HcompTop HiI).

An exact proof term for the current goal is (continuous_map_function_on X Tx (space_family_set Xi i) (space_family_topology Xi i) (product_eval_map I Xi i) Hcont).

We prove the intermediate claim Hcoord_nonempty: ∀i : set, i ∈ I → intersection_of_family (space_family_set Xi i) (Dproj i) ≠ Empty.

Let i be given.

Assume HiI: i ∈ I.

Set Xi0 to be the term space_family_set Xi i.

Set Ti0 to be the term space_family_topology Xi i.

We prove the intermediate claim Hcomp_i: compact_space Xi0 Ti0.

rewrite the current goal using (space_family_set_eq_product_component Xi i) (from left to right).

rewrite the current goal using (space_family_topology_eq_product_component_topology Xi i) (from left to right).

An exact proof term for the current goal is (Hcomp i HiI).

We prove the intermediate claim Htop_i: topology_on Xi0 Ti0.

An exact proof term for the current goal is (compact_space_topology Xi0 Ti0 Hcomp_i).

We prove the intermediate claim HclosedDi: ∀C : set, C ∈ (Dproj i) → closed_in Xi0 Ti0 C.

Let C be given.

Assume HC: C ∈ (Dproj i).

Apply (ReplE D (λE0 : set ⇒ closproj i E0) C HC) to the current goal.

Let E0 be given.

Assume HE0.

Apply HE0 to the current goal.

Assume HE0D: E0 ∈ D.

Assume HCeq: C = closproj i E0.

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

Apply (closure_is_closed Xi0 Ti0 (proj i E0) Htop_i) to the current goal.

Let y be given.

Assume Hy: y ∈ proj i E0.

Apply (ReplE E0 (λf0 : set ⇒ apply_fun (product_eval_map I Xi i) f0) y Hy) to the current goal.

Let f0 be given.

Assume Hf0.

Apply Hf0 to the current goal.

Assume Hf0E: f0 ∈ E0.

Assume Hyeq: y = apply_fun (product_eval_map I Xi i) f0.

We prove the intermediate claim HE0subX: E0 ⊆ X.

We prove the intermediate claim HE0Pow: E0 ∈ 𝒫 X.

An exact proof term for the current goal is (HDpow E0 HE0D).

An exact proof term for the current goal is (PowerE X E0 HE0Pow).

We prove the intermediate claim Hf0X: f0 ∈ X.

An exact proof term for the current goal is (HE0subX f0 Hf0E).

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

An exact proof term for the current goal is ((HevFun i HiI) f0 Hf0X).

We prove the intermediate claim HfipDi: finite_intersection_property Xi0 (Dproj i).

We will prove (Dproj i) ⊆ 𝒫 Xi0 ∧ ∀F : set, finite F → F ⊆ (Dproj i) → intersection_of_family Xi0 F ≠ Empty.

Apply andI to the current goal.

Let C be given.

Assume HC: C ∈ (Dproj i).

We prove the intermediate claim Hsub: C ⊆ Xi0.

Let y be given.

Assume HyC: y ∈ C.

Apply (ReplE D (λE0 : set ⇒ closproj i E0) C HC) to the current goal.

Let E0 be given.

Assume HE0.

Apply HE0 to the current goal.

Assume HE0D: E0 ∈ D.

Assume HCeq: C = closproj i E0.

We prove the intermediate claim HyC0: y ∈ closproj i E0.

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

An exact proof term for the current goal is HyC.

An exact proof term for the current goal is (SepE1 Xi0 (λx0 : set ⇒ ∀U : set, U ∈ Ti0 → x0 ∈ U → U ∩ proj i E0 ≠ Empty) y HyC0).

An exact proof term for the current goal is (PowerI Xi0 C Hsub).

Let F be given.

Assume HFfin: finite F.

Assume HFsub: F ⊆ (Dproj i).

Set pickE to be the term λC0 : set ⇒ Eps_i (λE0 : set ⇒ E0 ∈ D ∧ C0 = closproj i E0).

Set G to be the term {pickE C0|C0 ∈ F}.

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (Repl_finite pickE F HFfin).

We prove the intermediate claim HGsubD: G ⊆ D.

Let E0 be given.

Assume HE0: E0 ∈ G.

Apply (ReplE F (λC0 : set ⇒ pickE C0) E0 HE0) to the current goal.

Let C0 be given.

Assume HC0.

Apply HC0 to the current goal.

Assume HC0F: C0 ∈ F.

Assume HE0eq: E0 = pickE C0.

We prove the intermediate claim HC0Dproj: C0 ∈ (Dproj i).

An exact proof term for the current goal is (HFsub C0 HC0F).

We prove the intermediate claim HexE0: ∃E1 : set, E1 ∈ D ∧ C0 = closproj i E1.

An exact proof term for the current goal is (ReplE D (λE1 : set ⇒ closproj i E1) C0 HC0Dproj).

We prove the intermediate claim Hpick: pickE C0 ∈ D ∧ C0 = closproj i (pickE C0).

An exact proof term for the current goal is (Eps_i_ex (λE1 : set ⇒ E1 ∈ D ∧ C0 = closproj i E1) HexE0).

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

An exact proof term for the current goal is (andEL (pickE C0 ∈ D) (C0 = closproj i (pickE C0)) Hpick).

We prove the intermediate claim HinterG: intersection_of_family X G ≠ Empty.

An exact proof term for the current goal is (HDfip G HGfin HGsubD).

Apply (nonempty_has_element (intersection_of_family X G) HinterG) to the current goal.

Let p be given.

Assume HpG: p ∈ intersection_of_family X G.

Set pi to be the term product_eval_map I Xi i.

Set y to be the term apply_fun pi p.

Apply (elem_implies_nonempty (intersection_of_family Xi0 F) y) to the current goal.

We will prove y ∈ intersection_of_family Xi0 F.

We prove the intermediate claim HpX: p ∈ X.

An exact proof term for the current goal is (SepE1 X (λz : set ⇒ ∀T : set, T ∈ G → z ∈ T) p HpG).

We prove the intermediate claim HyXi0: y ∈ Xi0.

An exact proof term for the current goal is ((HevFun i HiI) p HpX).

We prove the intermediate claim HallF: ∀C0 : set, C0 ∈ F → y ∈ C0.

Let C0 be given.

Assume HC0F: C0 ∈ F.

We prove the intermediate claim HC0Dproj: C0 ∈ (Dproj i).

An exact proof term for the current goal is (HFsub C0 HC0F).

Set E0 to be the term pickE C0.

We prove the intermediate claim HE0inG: E0 ∈ G.

An exact proof term for the current goal is (ReplI F (λC1 : set ⇒ pickE C1) C0 HC0F).

We prove the intermediate claim HvalsG: ∀T : set, T ∈ G → p ∈ T.

An exact proof term for the current goal is (SepE2 X (λz : set ⇒ ∀T : set, T ∈ G → z ∈ T) p HpG).

We prove the intermediate claim HpE0: p ∈ E0.

An exact proof term for the current goal is (HvalsG E0 HE0inG).

We prove the intermediate claim HE0D: E0 ∈ D.

An exact proof term for the current goal is (HGsubD E0 HE0inG).

We prove the intermediate claim HE0subX: E0 ⊆ X.

An exact proof term for the current goal is (PowerE X E0 (HDpow E0 HE0D)).

We prove the intermediate claim HpX0: p ∈ X.

An exact proof term for the current goal is (HE0subX p HpE0).

We prove the intermediate claim Hy_in_proj: y ∈ proj i E0.

Set ev to be the term product_eval_map I Xi i.

We prove the intermediate claim Hyeq: y = apply_fun ev p.

Use reflexivity.

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

An exact proof term for the current goal is (ReplI E0 (λf0 : set ⇒ apply_fun ev f0) p HpE0).

We prove the intermediate claim HprojSub: proj i E0 ⊆ Xi0.

Let z be given.

Assume Hz: z ∈ proj i E0.

Apply (ReplE E0 (λf0 : set ⇒ apply_fun (product_eval_map I Xi i) f0) z Hz) to the current goal.

Let f0 be given.

Assume Hf0.

Apply Hf0 to the current goal.

Assume Hf0E0: f0 ∈ E0.

Assume Hzeq: z = apply_fun (product_eval_map I Xi i) f0.

We prove the intermediate claim Hf0X: f0 ∈ X.

An exact proof term for the current goal is (HE0subX f0 Hf0E0).

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

An exact proof term for the current goal is ((HevFun i HiI) f0 Hf0X).

We prove the intermediate claim Hy_in_clos: y ∈ closure_of Xi0 Ti0 (proj i E0).

An exact proof term for the current goal is (subset_of_closure Xi0 Ti0 (proj i E0) Htop_i HprojSub y Hy_in_proj).

We prove the intermediate claim HexE0: ∃E1 : set, E1 ∈ D ∧ C0 = closproj i E1.

An exact proof term for the current goal is (ReplE D (λE1 : set ⇒ closproj i E1) C0 HC0Dproj).

We prove the intermediate claim Hpick: E0 ∈ D ∧ C0 = closproj i E0.

An exact proof term for the current goal is (Eps_i_ex (λE1 : set ⇒ E1 ∈ D ∧ C0 = closproj i E1) HexE0).

We prove the intermediate claim HC0eq: C0 = closproj i E0.

An exact proof term for the current goal is (andER (E0 ∈ D) (C0 = closproj i E0) Hpick).

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

An exact proof term for the current goal is Hy_in_clos.

An exact proof term for the current goal is (intersection_of_familyI Xi0 F y HyXi0 HallF).

An exact proof term for the current goal is (compact_space_closed_FIP_intersection_nonempty Xi0 Ti0 (Dproj i) Hcomp_i HclosedDi HfipDi).

Set xi to be the term (λi : set ⇒ Eps_i (λy : set ⇒ y ∈ intersection_of_family (space_family_set Xi i) (Dproj i))).

We prove the intermediate claim Hxi: ∀i : set, i ∈ I → xi i ∈ intersection_of_family (space_family_set Xi i) (Dproj i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hne: intersection_of_family (space_family_set Xi i) (Dproj i) ≠ Empty.

An exact proof term for the current goal is (Hcoord_nonempty i HiI).

We prove the intermediate claim Hexy: ∃y : set, y ∈ intersection_of_family (space_family_set Xi i) (Dproj i).

An exact proof term for the current goal is (nonempty_has_element (intersection_of_family (space_family_set Xi i) (Dproj i)) Hne).

An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ intersection_of_family (space_family_set Xi i) (Dproj i)) Hexy).

Set x to be the term graph I (λi : set ⇒ xi i).

We prove the intermediate claim HxX: x ∈ X.

Apply (product_space_graphI I Xi (λi0 : set ⇒ xi i0)) to the current goal.

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim HxiInt: xi i ∈ intersection_of_family (space_family_set Xi i) (Dproj i).

An exact proof term for the current goal is (Hxi i HiI).

An exact proof term for the current goal is (SepE1 (space_family_set Xi i) (λy0 : set ⇒ ∀C0 : set, C0 ∈ Dproj i → y0 ∈ C0) (xi i) HxiInt).

We prove the intermediate claim Hsub_in_D: ∀s : set, s ∈ S → x ∈ s → s ∈ D.

Let s be given.

Assume HsS: s ∈ S.

Assume Hxs: x ∈ s.

Apply (product_subbasis_fullE I Xi s HsS) to the current goal.

Let i be given.

Assume Hipack.

Apply Hipack to the current goal.

Assume HiI HexU.

Apply HexU to the current goal.

Let U be given.

Assume HUand.

We prove the intermediate claim HUtop: U ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (s = product_cylinder I Xi i U) HUand).

We prove the intermediate claim Hseq: s = product_cylinder I Xi i U.

An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder I Xi i U) HUand).

Set cyl to be the term product_cylinder I Xi i U.

We prove the intermediate claim Hxcyl: x ∈ cyl.

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

An exact proof term for the current goal is Hxs.

We prove the intermediate claim HcylSubX: cyl ⊆ X.

Let f be given.

Assume Hf: f ∈ cyl.

An exact proof term for the current goal is (SepE1 X (λg : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f Hf).

We prove the intermediate claim Hmeet: ∀B : set, B ∈ D → cyl ∩ B ≠ Empty.

Let B be given.

Assume HB: B ∈ D.

We prove the intermediate claim HxiInt: xi i ∈ intersection_of_family (space_family_set Xi i) (Dproj i).

An exact proof term for the current goal is (Hxi i HiI).

We prove the intermediate claim Hcl_in_Dproj: closproj i B ∈ Dproj i.

An exact proof term for the current goal is (ReplI D (λE0 : set ⇒ closproj i E0) B HB).

We prove the intermediate claim HxiInCl: xi i ∈ closproj i B.

An exact proof term for the current goal is (SepE2 (space_family_set Xi i) (λy0 : set ⇒ ∀C0 : set, C0 ∈ Dproj i → y0 ∈ C0) (xi i) HxiInt (closproj i B) Hcl_in_Dproj).

We prove the intermediate claim HxiU: xi i ∈ U.

We prove the intermediate claim HxcylProp: i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun x i ∈ U.

An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) x Hxcyl).

We prove the intermediate claim HxU: apply_fun x i ∈ U.

An exact proof term for the current goal is (andER (i ∈ I ∧ U ∈ space_family_topology Xi i) (apply_fun x i ∈ U) HxcylProp).

We prove the intermediate claim HxEq0: apply_fun x i = (λj0 : set ⇒ xi j0) i.

An exact proof term for the current goal is (apply_fun_graph I (λj0 : set ⇒ xi j0) i HiI).

We prove the intermediate claim HxEq: apply_fun x i = xi i.

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

Use reflexivity.

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

An exact proof term for the current goal is HxU.

We prove the intermediate claim HUi: U ∩ proj i B ≠ Empty.

An exact proof term for the current goal is (SepE2 (space_family_set Xi i) (λy0 : set ⇒ ∀V : set, V ∈ space_family_topology Xi i → y0 ∈ V → V ∩ proj i B ≠ Empty) (xi i) HxiInCl U HUtop HxiU).

Apply (nonempty_has_element (U ∩ proj i B) HUi) to the current goal.

Let y0 be given.

Assume Hy0: y0 ∈ (U ∩ proj i B).

We prove the intermediate claim Hy0U: y0 ∈ U.

An exact proof term for the current goal is (binintersectE1 U (proj i B) y0 Hy0).

We prove the intermediate claim Hy0Proj: y0 ∈ proj i B.

An exact proof term for the current goal is (binintersectE2 U (proj i B) y0 Hy0).

Apply (ReplE B (λf0 : set ⇒ apply_fun (product_eval_map I Xi i) f0) y0 Hy0Proj) to the current goal.

Let f0 be given.

Assume Hf0.

Apply Hf0 to the current goal.

Assume Hf0B: f0 ∈ B.

Assume Hy0eq: y0 = apply_fun (product_eval_map I Xi i) f0.

Apply (elem_implies_nonempty (cyl ∩ B) f0) to the current goal.

We will prove f0 ∈ cyl ∩ B.

Apply binintersectI to the current goal.

We will prove f0 ∈ cyl.

We prove the intermediate claim Hf0X: f0 ∈ X.

An exact proof term for the current goal is ((PowerE X B (HDpow B HB)) f0 Hf0B).

We prove the intermediate claim HcylDef: cyl = {g ∈ X|i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.

Use reflexivity.

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

Apply (SepI X (λg : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f0 Hf0X) to the current goal.

We will prove i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is HiI.

An exact proof term for the current goal is HUtop.

Set ev to be the term product_eval_map I Xi i.

We prove the intermediate claim Hev: apply_fun ev f0 = apply_fun f0 i.

An exact proof term for the current goal is (apply_fun_graph X (λg0 : set ⇒ apply_fun g0 i) f0 Hf0X).

We prove the intermediate claim Hy0eqi: y0 = apply_fun f0 i.

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

An exact proof term for the current goal is Hev.

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

An exact proof term for the current goal is Hy0U.

An exact proof term for the current goal is Hf0B.

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

An exact proof term for the current goal is (Lemma37_2b_max_fip_meets_all_implies_in X D cyl HmaxD HcylSubX Hmeet).

We prove the intermediate claim Hbasis_in_D: ∀b : set, b ∈ basis_of_subbasis X S → x ∈ b → b ∈ D.

Let b be given.

Assume HbB: b ∈ basis_of_subbasis X S.

Assume Hxb: x ∈ b.

Apply (basis_of_subbasisE X S b HbB) to the current goal.

Let F be given.

Assume HFpack.

Apply HFpack to the current goal.

Assume HFand HbNe.

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

An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (b = intersection_of_family X F) HFand).

We prove the intermediate claim HbEq: b = intersection_of_family X F.

An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (b = intersection_of_family X F) HFand).

We prove the intermediate claim HFmem: F ∈ {F0 ∈ 𝒫 S|finite F0}.

We prove the intermediate claim HFdef: finite_subcollections S = {F0 ∈ 𝒫 S|finite F0}.

Use reflexivity.

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

An exact proof term for the current goal is HFfinSub.

We prove the intermediate claim HFfin: finite F.

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

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

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

We prove the intermediate claim HFsubS: F ⊆ S.

An exact proof term for the current goal is (PowerE S F HFpow).

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

We prove the intermediate claim HFsubD: F ⊆ D.

Let s be given.

Assume HsF: s ∈ F.

We prove the intermediate claim HsS: s ∈ S.

An exact proof term for the current goal is (HFsubS s HsF).

We prove the intermediate claim HxInInt: x ∈ intersection_of_family X F.

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

An exact proof term for the current goal is Hxb.

We prove the intermediate claim HxX0: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λz : set ⇒ ∀T : set, T ∈ F → z ∈ T) x HxInInt).

We prove the intermediate claim HallF: ∀T : set, T ∈ F → x ∈ T.

An exact proof term for the current goal is (SepE2 X (λz : set ⇒ ∀T : set, T ∈ F → z ∈ T) x HxInInt).

We prove the intermediate claim Hxs: x ∈ s.

An exact proof term for the current goal is (HallF s HsF).

An exact proof term for the current goal is (Hsub_in_D s HsS Hxs).

An exact proof term for the current goal is (Lemma37_2a_max_fip_finite_intersections_in X D HmaxD F HFfin HFsubD).

We prove the intermediate claim HxInA: ∀C : set, C ∈ A → x ∈ C.

Let C be given.

Assume HCA: C ∈ A.

We prove the intermediate claim HCD: C ∈ D.

An exact proof term for the current goal is (HAsubD C HCA).

We prove the intermediate claim HCclosed: closed_in X Tx C.

An exact proof term for the current goal is (HclosedA C HCA).

We prove the intermediate claim Hxcl: x ∈ closure_of X Tx C.

We prove the intermediate claim Hnbhd: ∀U : set, U ∈ Tx → x ∈ U → U ∩ C ≠ Empty.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We prove the intermediate claim HUgen: U ∈ generated_topology_from_subbasis X S.

We prove the intermediate claim HTdef: Tx = generated_topology_from_subbasis X S.

Use reflexivity.

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

An exact proof term for the current goal is HU.

We prove the intermediate claim Hexb: ∃b : set, b ∈ basis_of_subbasis X S ∧ x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (generated_topology_from_subbasis_local_basis X S U x HUgen HxU).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpack.

We prove the intermediate claim Hb12: b ∈ basis_of_subbasis X S ∧ x ∈ b.

An exact proof term for the current goal is (andEL (b ∈ basis_of_subbasis X S ∧ x ∈ b) (b ⊆ U) Hbpack).

We prove the intermediate claim HbB: b ∈ basis_of_subbasis X S.

An exact proof term for the current goal is (andEL (b ∈ basis_of_subbasis X S) (x ∈ b) Hb12).

We prove the intermediate claim Hxb: x ∈ b.

An exact proof term for the current goal is (andER (b ∈ basis_of_subbasis X S) (x ∈ b) Hb12).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ basis_of_subbasis X S ∧ x ∈ b) (b ⊆ U) Hbpack).

We prove the intermediate claim HbD: b ∈ D.

An exact proof term for the current goal is (Hbasis_in_D b HbB Hxb).

Set F0 to be the term {b} ∪ {C}.

We prove the intermediate claim HF0fin: finite F0.

An exact proof term for the current goal is (binunion_finite {b} (Sing_finite b) {C} (Sing_finite C)).

We prove the intermediate claim HF0subD: F0 ⊆ D.

Let T be given.

Assume HT: T ∈ F0.

Apply (binunionE' {b} {C} T (T ∈ D)) to the current goal.

Assume HTb: T ∈ {b}.

We prove the intermediate claim HTeq: T = b.

An exact proof term for the current goal is (SingE b T HTb).

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

An exact proof term for the current goal is HbD.

Assume HTc: T ∈ {C}.

We prove the intermediate claim HTeq: T = C.

An exact proof term for the current goal is (SingE C T HTc).

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

An exact proof term for the current goal is HCD.

An exact proof term for the current goal is HT.

We prove the intermediate claim Hnon: intersection_of_family X F0 ≠ Empty.

An exact proof term for the current goal is (HDfip F0 HF0fin HF0subD).

Apply (nonempty_has_element (intersection_of_family X F0) Hnon) to the current goal.

Let y be given.

Assume Hy: y ∈ intersection_of_family X F0.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λz : set ⇒ ∀T : set, T ∈ F0 → z ∈ T) y Hy).

We prove the intermediate claim Hall: ∀T : set, T ∈ F0 → y ∈ T.

An exact proof term for the current goal is (SepE2 X (λz : set ⇒ ∀T : set, T ∈ F0 → z ∈ T) y Hy).

We prove the intermediate claim Hyb: y ∈ b.

Apply (Hall b) to the current goal.

An exact proof term for the current goal is (binunionI1 {b} {C} b (SingI b)).

We prove the intermediate claim HyC: y ∈ C.

Apply (Hall C) to the current goal.

An exact proof term for the current goal is (binunionI2 {b} {C} C (SingI C)).

Apply (elem_implies_nonempty (U ∩ C) y) to the current goal.

We will prove y ∈ U ∩ C.

Apply binintersectI to the current goal.

An exact proof term for the current goal is (HbsubU y Hyb).

An exact proof term for the current goal is HyC.

An exact proof term for the current goal is (SepI X (λz : set ⇒ ∀U0 : set, U0 ∈ Tx → z ∈ U0 → U0 ∩ C ≠ Empty) x HxX Hnbhd).

rewrite the current goal using (closed_closure_eq X Tx C HTx HCclosed) (from right to left) at position 1.

An exact proof term for the current goal is Hxcl.

Apply (elem_implies_nonempty (intersection_of_family X A) x) to the current goal.

We will prove x ∈ intersection_of_family X A.

An exact proof term for the current goal is (intersection_of_familyI X A x HxX (λC0 HC0 ⇒ HxInA C0 HC0)).