Let a, b, c and d be given.
Assume Hab: Rlt a b.
Assume Hcd: Rlt c d.
rewrite the current goal using (open_rectangle_set_eq_rectangle_set_intervals a b c d) (from left to right).
We prove the intermediate claim HU: open_interval a b ∈ R_standard_topology.
An exact proof term for the current goal is (open_interval_in_R_standard_topology a b Hab).
We prove the intermediate claim HV: open_interval c d ∈ R_standard_topology.
An exact proof term for the current goal is (open_interval_in_R_standard_topology c d Hcd).
We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HrectInFam: rectangle_set (open_interval a b) (open_interval c d) ∈ {rectangle_set (open_interval a b) V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV0 : set ⇒ rectangle_set (open_interval a b) V0) (open_interval c d) HV).
We prove the intermediate claim HrectInSub: rectangle_set (open_interval a b) (open_interval c d) ∈ 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_interval a b) (rectangle_set (open_interval a b) (open_interval c d)) HU HrectInFam).
We prove the intermediate claim HrectPow: rectangle_set (open_interval a b) (open_interval c d) ∈ 𝒫 (setprod R R).
Apply PowerI to the current goal.
Let p be given.
Assume Hp: p ∈ rectangle_set (open_interval a b) (open_interval c d).
We will prove p ∈ setprod R R.
We prove the intermediate claim HpUV: p ∈ setprod (open_interval a b) (open_interval c d).
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_interval a b.
An exact proof term for the current goal is (ap0_Sigma (open_interval a b) (λ_ : set ⇒ open_interval c d) p HpUV).
We prove the intermediate claim Hp1V: p 1 ∈ open_interval c d.
An exact proof term for the current goal is (ap1_Sigma (open_interval a b) (λ_ : set ⇒ open_interval c d) p HpUV).
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a z ∧ Rlt z b) (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 ⇒ Rlt c z ∧ Rlt z d) (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_interval a b) (open_interval c d) 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_interval a b) (open_interval c d)) HrectPow HrectInSub).
∎