Let q be given.
Assume HqR: q ∈ R.
We will prove rectangle_set (open_ray_upper R q) (open_ray_lower R q) ∈ R2_standard_topology.
We prove the intermediate claim HU: open_ray_upper R q ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_upper_in_R_standard_topology q HqR).
We prove the intermediate claim HV: open_ray_lower R q ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_lower_in_R_standard_topology q HqR).
We prove the intermediate claim HrectInFam: rectangle_set (open_ray_upper R q) (open_ray_lower R q) ∈ {rectangle_set (open_ray_upper R q) V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV0 : set ⇒ rectangle_set (open_ray_upper R q) V0) (open_ray_lower R q) HV).
We prove the intermediate claim HrectInSub: rectangle_set (open_ray_upper R q) (open_ray_lower R q) ∈ product_subbasis R R_standard_topology R R_standard_topology.
An exact proof term for the current goal is (famunionI R_standard_topology (λU0 : set ⇒ {rectangle_set U0 V|V ∈ R_standard_topology}) (open_ray_upper R q) (rectangle_set (open_ray_upper R q) (open_ray_lower R q)) HU HrectInFam).
We prove the intermediate claim HrectPow: rectangle_set (open_ray_upper R q) (open_ray_lower R q) ∈ 𝒫 (setprod R R).
Apply PowerI to the current goal.
Let p be given.
Assume Hp: p ∈ rectangle_set (open_ray_upper R q) (open_ray_lower R q).
We will prove p ∈ setprod R R.
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 left to right).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hp0U: 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 Hp1V: 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 Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ order_rel R q z) (p 0) Hp0U).
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) Hp1V).
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).
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 (generated_topology_contains_elem (setprod R R) (product_subbasis R R_standard_topology R R_standard_topology) (rectangle_set (open_ray_upper R q) (open_ray_lower R q)) HrectPow HrectInSub).
∎