Set Gt to be the term {p ∈ EuclidPlane|Rlt (p 1) (p 0)}.
Set Fam to be the term {rectangle_set (open_ray_upper R q) (open_ray_lower R q)|q ∈ rational_numbers}.
We prove the intermediate claim HPlaneDef: EuclidPlane = setprod R R.
Use reflexivity.
We prove the intermediate claim HGtEq: Gt = ⋃ Fam.
Apply set_ext to the current goal.
Let p be given.
Assume HpGt: p ∈ Gt.
We will prove p ∈ ⋃ Fam.
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (p0 1) (p0 0)) p HpGt).
We prove the intermediate claim Hp10: Rlt (p 1) (p 0).
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (p0 1) (p0 0)) p HpGt).
We prove the intermediate claim HpRR: p ∈ setprod R R.
rewrite the current goal using HPlaneDef (from right to left).
An exact proof term for the current goal is HpE.
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hp1R: p 1 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt (p 1) q ∧ Rlt q (p 0).
An exact proof term for the current goal is (rational_dense_between_reals (p 1) (p 0) Hp1R Hp0R Hp10).
Apply Hexq to the current goal.
Let q be given.
Assume Hqcore.
Apply Hqcore to the current goal.
Assume HqQ Hqineq.
We prove the intermediate claim Hp1q: Rlt (p 1) q.
An exact proof term for the current goal is (andEL (Rlt (p 1) q) (Rlt q (p 0)) Hqineq).
We prove the intermediate claim Hq0: Rlt q (p 0).
An exact proof term for the current goal is (andER (Rlt (p 1) q) (Rlt q (p 0)) Hqineq).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hp0Up: p 0 ∈ open_ray_upper R q.
We prove the intermediate claim Hrel: order_rel R q (p 0).
An exact proof term for the current goal is (Rlt_implies_order_rel_R q (p 0) Hq0).
An exact proof term for the current goal is (SepI R (λz : set ⇒ order_rel R q z) (p 0) Hp0R Hrel).
We prove the intermediate claim Hp1Low: p 1 ∈ open_ray_lower R q.
We prove the intermediate claim Hrel: order_rel R (p 1) q.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (p 1) q Hp1q).
An exact proof term for the current goal is (SepI R (λz : set ⇒ order_rel R z q) (p 1) Hp1R Hrel).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
Set U to be the term rectangle_set (open_ray_upper R q) (open_ray_lower R q).
We prove the intermediate claim HpU: p ∈ U.
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_rectangle_set (open_ray_upper R q) (open_ray_lower R q) (p 0) (p 1) Hp0Up Hp1Low).
We prove the intermediate claim HUinFam: U ∈ Fam.
An exact proof term for the current goal is (ReplI rational_numbers (λq0 : set ⇒ rectangle_set (open_ray_upper R q0) (open_ray_lower R q0)) q HqQ).
An exact proof term for the current goal is (UnionI Fam p U HpU HUinFam).
Let p be given.
Assume HpUnion: p ∈ ⋃ Fam.
We will prove p ∈ Gt.
Apply (UnionE_impred Fam p HpUnion (p ∈ Gt)) to the current goal.
Let U be given.
Assume HpU: p ∈ U.
Assume HUfam: U ∈ Fam.
Apply (ReplE_impred rational_numbers (λq0 : set ⇒ rectangle_set (open_ray_upper R q0) (open_ray_lower R q0)) U HUfam (p ∈ Gt)) to the current goal.
Let q be given.
Assume HqQ: q ∈ rational_numbers.
Assume HUeq: U = rectangle_set (open_ray_upper R q) (open_ray_lower R q).
We prove the intermediate claim HpUV: p ∈ setprod (open_ray_upper R q) (open_ray_lower R q).
rewrite the current goal using rectangle_set_def (from right to left).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HpU.
We prove the intermediate claim Hp0Up: p 0 ∈ open_ray_upper R q.
An exact proof term for the current goal is (ap0_Sigma (open_ray_upper R q) (λ_ : set ⇒ open_ray_lower R q) p HpUV).
We prove the intermediate claim Hp1Low: p 1 ∈ open_ray_lower R q.
An exact proof term for the current goal is (ap1_Sigma (open_ray_upper R q) (λ_ : set ⇒ open_ray_lower R q) p HpUV).
We prove the intermediate claim H0rel: order_rel R q (p 0).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ order_rel R q z) (p 0) Hp0Up).
We prove the intermediate claim H1rel: order_rel R (p 1) q.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ order_rel R z q) (p 1) Hp1Low).
We prove the intermediate claim Hp1q: Rlt (p 1) q.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (p 1) q H1rel).
We prove the intermediate claim Hq0: Rlt q (p 0).
An exact proof term for the current goal is (order_rel_R_implies_Rlt q (p 0) H0rel).
We prove the intermediate claim Hp10: Rlt (p 1) (p 0).
An exact proof term for the current goal is (Rlt_tra (p 1) q (p 0) Hp1q Hq0).
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ order_rel R q z) (p 0) Hp0Up).
We prove the intermediate claim Hp1R: p 1 ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ order_rel R z q) (p 1) Hp1Low).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta (open_ray_upper R q) (open_ray_lower R q) p HpUV).
We prove the intermediate claim HpE: p ∈ EuclidPlane.
rewrite the current goal using HPlaneDef (from left to right).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (p 0) (p 1) Hp0R Hp1R).
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (p0 1) (p0 0)) p HpE Hp10).
We prove the intermediate claim HT: topology_on EuclidPlane R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology_local R_standard_topology_is_topology_local).
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 R2_standard_topology.
Apply PowerI to the current goal.
Let U be given.
Assume HU: U ∈ Fam.
We will prove U ∈ R2_standard_topology.
Apply (ReplE_impred rational_numbers (λq0 : set ⇒ rectangle_set (open_ray_upper R q0) (open_ray_lower R q0)) U HU (U ∈ R2_standard_topology)) to the current goal.
Let q be given.
Assume HqQ: q ∈ rational_numbers.
Assume HUeq: U = rectangle_set (open_ray_upper R q) (open_ray_lower R q).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (open_ray_rectangle_swapped_in_R2_standard_topology q HqR).
We prove the intermediate claim HUnionOpen: ⋃ Fam ∈ R2_standard_topology.
An exact proof term for the current goal is (topology_union_closed_pow EuclidPlane R2_standard_topology Fam HT HFamPow).
rewrite the current goal using HGtEq (from left to right).
An exact proof term for the current goal is HUnionOpen.
∎