Let p be given.

Assume Hp: p ∈ closure_of Xprod Tprod P.

We will prove p ∈ setprod clA clB.

We prove the intermediate claim HpXprod: p ∈ Xprod.

An exact proof term for the current goal is (SepE1 Xprod (λp0 ⇒ ∀W : set, W ∈ Tprod → p0 ∈ W → W ∩ P ≠ Empty) p Hp).

We prove the intermediate claim Hpcl: ∀W : set, W ∈ Tprod → p ∈ W → W ∩ P ≠ Empty.

An exact proof term for the current goal is (SepE2 Xprod (λp0 ⇒ ∀W : set, W ∈ Tprod → p0 ∈ W → W ∩ P ≠ Empty) p Hp).

Apply (setprod_elem_decompose X Y p HpXprod) to the current goal.

Let x be given.

Assume Hxconj.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hxconj).

Apply (andER (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hxconj) to the current goal.

Let y be given.

Assume Hyconj.

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (andEL (y ∈ Y) (p ∈ setprod {x} {y}) Hyconj).

We prove the intermediate claim HpXYsing: p ∈ setprod {x} {y}.

An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {x} {y}) Hyconj).

We prove the intermediate claim HxclA: x ∈ clA.

We will prove x ∈ closure_of X Tx A.

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

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

Set WY to be the term rectangle_set U Y.

We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).

An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).

We prove the intermediate claim HYopen: Y ∈ Ty.

An exact proof term for the current goal is (topology_has_X Y Ty HTy).

We prove the intermediate claim HWYsub: WY ∈ product_subbasis X Tx Y Ty.

We will prove WY ∈ product_subbasis X Tx Y Ty.

We prove the intermediate claim HWYV: rectangle_set U Y ∈ {rectangle_set U V|V ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV1 : set ⇒ rectangle_set U V1) Y HYopen).

An exact proof term for the current goal is (famunionI Tx (λU1 : set ⇒ {rectangle_set U1 V|V ∈ Ty}) U (rectangle_set U Y) HU HWYV).

We prove the intermediate claim HWYopen: WY ∈ Tprod.

An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis WY HWYsub).

We prove the intermediate claim HpWY: p ∈ WY.

We prove the intermediate claim Hsx: {x} ⊆ U.

An exact proof term for the current goal is (singleton_subset x U HxU).

We prove the intermediate claim Hsy: {y} ⊆ Y.

An exact proof term for the current goal is (singleton_subset y Y HyY).

We prove the intermediate claim Hsub: setprod {x} {y} ⊆ setprod U Y.

An exact proof term for the current goal is (setprod_Subq {x} {y} U Y Hsx Hsy).

An exact proof term for the current goal is (Hsub p HpXYsing).

We prove the intermediate claim Hnonemp: WY ∩ P ≠ Empty.

An exact proof term for the current goal is (Hpcl WY HWYopen HpWY).

Apply (nonempty_has_element (WY ∩ P) Hnonemp) to the current goal.

Let q be given.

Assume HqInt.

We prove the intermediate claim HqWY: q ∈ WY.

An exact proof term for the current goal is (binintersectE1 WY P q HqInt).

We prove the intermediate claim HqP: q ∈ P.

An exact proof term for the current goal is (binintersectE2 WY P q HqInt).

Apply (setprod_elem_decompose A B q HqP) to the current goal.

Let a be given.

Assume Haconj.

We prove the intermediate claim HaA: a ∈ A.

An exact proof term for the current goal is (andEL (a ∈ A) (∃b ∈ B, q ∈ setprod {a} {b}) Haconj).

Apply (andER (a ∈ A) (∃b ∈ B, q ∈ setprod {a} {b}) Haconj) to the current goal.

Let b be given.

Assume Hbconj.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (q ∈ setprod {a} {b}) Hbconj).

We prove the intermediate claim Hqabsing: q ∈ setprod {a} {b}.

An exact proof term for the current goal is (andER (b ∈ B) (q ∈ setprod {a} {b}) Hbconj).

We prove the intermediate claim Hcoords: a ∈ U ∧ b ∈ Y.

An exact proof term for the current goal is (setprod_coords_in a b U Y q Hqabsing HqWY).

We prove the intermediate claim HaU: a ∈ U.

An exact proof term for the current goal is (andEL (a ∈ U) (b ∈ Y) Hcoords).

We prove the intermediate claim HaUA: a ∈ U ∩ A.

An exact proof term for the current goal is (binintersectI U A a HaU HaA).

We will prove U ∩ A ≠ Empty.

Assume Hempty: U ∩ A = Empty.

We prove the intermediate claim HaE: a ∈ Empty.

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

An exact proof term for the current goal is HaUA.

An exact proof term for the current goal is (EmptyE a HaE).

An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hxcond).

We prove the intermediate claim HyclB: y ∈ clB.

We will prove y ∈ closure_of Y Ty B.

We prove the intermediate claim Hycond: ∀V : set, V ∈ Ty → y ∈ V → V ∩ B ≠ Empty.

Let V be given.

Assume HV: V ∈ Ty.

Assume HyV: y ∈ V.

Set WX to be the term rectangle_set X V.

We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).

An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).

We prove the intermediate claim HXopen: X ∈ Tx.

An exact proof term for the current goal is (topology_has_X X Tx HTx).

We prove the intermediate claim HWXsub: WX ∈ product_subbasis X Tx Y Ty.

We will prove WX ∈ product_subbasis X Tx Y Ty.

We prove the intermediate claim HWXV: rectangle_set X V ∈ {rectangle_set X V0|V0 ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV1 : set ⇒ rectangle_set X V1) V HV).

An exact proof term for the current goal is (famunionI Tx (λU1 : set ⇒ {rectangle_set U1 V0|V0 ∈ Ty}) X (rectangle_set X V) HXopen HWXV).

We prove the intermediate claim HWXopen: WX ∈ Tprod.

An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis WX HWXsub).

We prove the intermediate claim HpWX: p ∈ WX.

We prove the intermediate claim Hsx: {x} ⊆ X.

An exact proof term for the current goal is (singleton_subset x X HxX).

We prove the intermediate claim Hsy: {y} ⊆ V.

An exact proof term for the current goal is (singleton_subset y V HyV).

We prove the intermediate claim Hsub: setprod {x} {y} ⊆ setprod X V.

An exact proof term for the current goal is (setprod_Subq {x} {y} X V Hsx Hsy).

An exact proof term for the current goal is (Hsub p HpXYsing).

We prove the intermediate claim Hnonemp: WX ∩ P ≠ Empty.

An exact proof term for the current goal is (Hpcl WX HWXopen HpWX).

Apply (nonempty_has_element (WX ∩ P) Hnonemp) to the current goal.

Let q be given.

Assume HqInt.

We prove the intermediate claim HqWX: q ∈ WX.

An exact proof term for the current goal is (binintersectE1 WX P q HqInt).

We prove the intermediate claim HqP: q ∈ P.

An exact proof term for the current goal is (binintersectE2 WX P q HqInt).

Apply (setprod_elem_decompose A B q HqP) to the current goal.

Let a be given.

Assume Haconj.

We prove the intermediate claim HaA: a ∈ A.

An exact proof term for the current goal is (andEL (a ∈ A) (∃b ∈ B, q ∈ setprod {a} {b}) Haconj).

Apply (andER (a ∈ A) (∃b ∈ B, q ∈ setprod {a} {b}) Haconj) to the current goal.

Let b be given.

Assume Hbconj.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (q ∈ setprod {a} {b}) Hbconj).

We prove the intermediate claim Hqabsing: q ∈ setprod {a} {b}.

An exact proof term for the current goal is (andER (b ∈ B) (q ∈ setprod {a} {b}) Hbconj).

We prove the intermediate claim Hcoords: a ∈ X ∧ b ∈ V.

An exact proof term for the current goal is (setprod_coords_in a b X V q Hqabsing HqWX).

We prove the intermediate claim HbV: b ∈ V.

An exact proof term for the current goal is (andER (a ∈ X) (b ∈ V) Hcoords).

We prove the intermediate claim HbVB: b ∈ V ∩ B.

An exact proof term for the current goal is (binintersectI V B b HbV HbB).

We will prove V ∩ B ≠ Empty.

Assume Hempty: V ∩ B = Empty.

We prove the intermediate claim HbE: b ∈ Empty.

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

An exact proof term for the current goal is HbVB.

An exact proof term for the current goal is (EmptyE b HbE).

An exact proof term for the current goal is (SepI Y (λy0 ⇒ ∀V : set, V ∈ Ty → y0 ∈ V → V ∩ B ≠ Empty) y HyY Hycond).

We prove the intermediate claim Hsx: {x} ⊆ clA.

An exact proof term for the current goal is (singleton_subset x clA HxclA).

We prove the intermediate claim Hsy: {y} ⊆ clB.

An exact proof term for the current goal is (singleton_subset y clB HyclB).

We prove the intermediate claim Hsub: setprod {x} {y} ⊆ setprod clA clB.

An exact proof term for the current goal is (setprod_Subq {x} {y} clA clB Hsx Hsy).

An exact proof term for the current goal is (Hsub p HpXYsing).

Let p be given.

Assume Hp: p ∈ setprod clA clB.

We will prove p ∈ closure_of Xprod Tprod P.

We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).

An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).

We prove the intermediate claim HTprod: topology_on (setprod X Y) Tprod.

An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).

Apply (setprod_elem_decompose clA clB p Hp) to the current goal.

Let x be given.

Assume Hxconj.

We prove the intermediate claim HxclA: x ∈ clA.

An exact proof term for the current goal is (andEL (x ∈ clA) (∃y ∈ clB, p ∈ setprod {x} {y}) Hxconj).

Apply (andER (x ∈ clA) (∃y ∈ clB, p ∈ setprod {x} {y}) Hxconj) to the current goal.

Let y be given.

Assume Hyconj.

We prove the intermediate claim HyclB: y ∈ clB.

An exact proof term for the current goal is (andEL (y ∈ clB) (p ∈ setprod {x} {y}) Hyconj).

We prove the intermediate claim HpXYsing: p ∈ setprod {x} {y}.

An exact proof term for the current goal is (andER (y ∈ clB) (p ∈ setprod {x} {y}) Hyconj).

We prove the intermediate claim HclAsubX: clA ⊆ X.

An exact proof term for the current goal is (closure_in_space X Tx A HTx).

We prove the intermediate claim HclBsubY: clB ⊆ Y.

An exact proof term for the current goal is (closure_in_space Y Ty B HTy).

We prove the intermediate claim HpXprod: p ∈ Xprod.

We prove the intermediate claim Hsub: setprod clA clB ⊆ setprod X Y.

An exact proof term for the current goal is (setprod_Subq clA clB X Y HclAsubX HclBsubY).

An exact proof term for the current goal is (Hsub p Hp).

We prove the intermediate claim Hpcond: ∀W : set, W ∈ Tprod → p ∈ W → W ∩ P ≠ Empty.

Let W be given.

Assume HW: W ∈ Tprod.

Assume HpW: p ∈ W.

We prove the intermediate claim HWgen: W ∈ generated_topology (setprod X Y) (product_subbasis X Tx Y Ty).

An exact proof term for the current goal is HW.

We prove the intermediate claim HWprop: ∀p0 ∈ W, ∃b ∈ product_subbasis X Tx Y Ty, p0 ∈ b ∧ b ⊆ W.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ product_subbasis X Tx Y Ty, p0 ∈ b ∧ b ⊆ U0) W HWgen).

We prove the intermediate claim Hexb: ∃b ∈ product_subbasis X Tx Y Ty, p ∈ b ∧ b ⊆ W.

An exact proof term for the current goal is (HWprop p HpW).

Apply Hexb to the current goal.

Let b be given.

Assume Hbconj.

We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx Y Ty.

An exact proof term for the current goal is (andEL (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ W) Hbconj).

We prove the intermediate claim Hpb: p ∈ b.

An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ W) (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ W) Hbconj)).

We prove the intermediate claim HbW: b ⊆ W.

An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ W) (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ W) Hbconj)).

Apply (famunionE Tx (λU1 : set ⇒ {rectangle_set U1 V|V ∈ Ty}) b HbSub) to the current goal.

Let U0 be given.

Assume HU0conj.

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).

We prove the intermediate claim HbInRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).

Apply (ReplE Ty (λV : set ⇒ rectangle_set U0 V) b HbInRepl) to the current goal.

Let V0 be given.

Assume HV0conj.

We prove the intermediate claim HV0Ty: V0 ∈ Ty.

An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).

We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.

An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).

We prove the intermediate claim HpbRect: p ∈ rectangle_set U0 V0.

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

An exact proof term for the current goal is Hpb.

We prove the intermediate claim Hcoords: x ∈ U0 ∧ y ∈ V0.

An exact proof term for the current goal is (setprod_coords_in x y U0 V0 p HpXYsing HpbRect).

We prove the intermediate claim HxU0: x ∈ U0.

An exact proof term for the current goal is (andEL (x ∈ U0) (y ∈ V0) Hcoords).

We prove the intermediate claim HyV0: y ∈ V0.

An exact proof term for the current goal is (andER (x ∈ U0) (y ∈ V0) Hcoords).

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

An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxclA).

We prove the intermediate claim HU0Ane: U0 ∩ A ≠ Empty.

An exact proof term for the current goal is (HxclAprop U0 HU0Tx HxU0).

Apply (nonempty_has_element (U0 ∩ A) HU0Ane) to the current goal.

Let a be given.

Assume HaUA.

We prove the intermediate claim HaU0: a ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 A a HaUA).

We prove the intermediate claim HaA: a ∈ A.

An exact proof term for the current goal is (binintersectE2 U0 A a HaUA).

We prove the intermediate claim HyclBprop: ∀V : set, V ∈ Ty → y ∈ V → V ∩ B ≠ Empty.

An exact proof term for the current goal is (SepE2 Y (λy0 ⇒ ∀V : set, V ∈ Ty → y0 ∈ V → V ∩ B ≠ Empty) y HyclB).

We prove the intermediate claim HV0Bne: V0 ∩ B ≠ Empty.

An exact proof term for the current goal is (HyclBprop V0 HV0Ty HyV0).

Apply (nonempty_has_element (V0 ∩ B) HV0Bne) to the current goal.

Let b0 be given.

Assume HbVB.

We prove the intermediate claim HbV0: b0 ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 B b0 HbVB).

We prove the intermediate claim HbB: b0 ∈ B.

An exact proof term for the current goal is (binintersectE2 V0 B b0 HbVB).

Set q to be the term (a,b0).

We prove the intermediate claim HqRect: q ∈ rectangle_set U0 V0.

An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 a b0 HaU0 HbV0).

We prove the intermediate claim Hqb: q ∈ b.

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

An exact proof term for the current goal is HqRect.

We prove the intermediate claim HqW: q ∈ W.

An exact proof term for the current goal is (HbW q Hqb).

We prove the intermediate claim HqP: q ∈ P.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A B a b0 HaA HbB).

Set I to be the term W ∩ P.

We prove the intermediate claim HqInt: q ∈ W ∩ P.

An exact proof term for the current goal is (binintersectI W P q HqW HqP).

An exact proof term for the current goal is (elem_implies_nonempty (W ∩ P) q HqInt).

An exact proof term for the current goal is (SepI Xprod (λp0 ⇒ ∀W : set, W ∈ Tprod → p0 ∈ W → W ∩ P ≠ Empty) p HpXprod Hpcond).