Let r be given.

Assume Hr: r ∈ rational_rectangle_basis.

We will prove r ∈ product_basis_from rational_open_intervals_basis rational_open_intervals_basis.

We prove the intermediate claim Hex: ∃a b c d : set, a ∈ rational_numbers ∧ b ∈ rational_numbers ∧ c ∈ rational_numbers ∧ d ∈ rational_numbers ∧ r = setprod (open_interval a b) (open_interval c d).

An exact proof term for the current goal is (SepE2 (𝒫 (setprod R R)) (λr0 : set ⇒ ∃a b c d : set, a ∈ rational_numbers ∧ b ∈ rational_numbers ∧ c ∈ rational_numbers ∧ d ∈ rational_numbers ∧ r0 = setprod (open_interval a b) (open_interval c d)) r Hr).

Apply Hex to the current goal.

Let a be given.

Assume H1.

Apply H1 to the current goal.

Let b be given.

Assume H2.

Apply H2 to the current goal.

Let c be given.

Assume H3.

Apply H3 to the current goal.

Let d be given.

Assume H4.

We prove the intermediate claim Hcore: a ∈ rational_numbers ∧ b ∈ rational_numbers ∧ c ∈ rational_numbers ∧ d ∈ rational_numbers ∧ r = setprod (open_interval a b) (open_interval c d).

An exact proof term for the current goal is H4.

We prove the intermediate claim Hleft: (((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) ∧ d ∈ rational_numbers) ∧ r = setprod (open_interval a b) (open_interval c d).

An exact proof term for the current goal is Hcore.

We prove the intermediate claim Hfour: ((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) ∧ d ∈ rational_numbers.

An exact proof term for the current goal is (andEL (((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) ∧ d ∈ rational_numbers) (r = setprod (open_interval a b) (open_interval c d)) Hleft).

We prove the intermediate claim Hreq: r = setprod (open_interval a b) (open_interval c d).

An exact proof term for the current goal is (andER (((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) ∧ d ∈ rational_numbers) (r = setprod (open_interval a b) (open_interval c d)) Hleft).

We prove the intermediate claim Hthree: (a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers.

An exact proof term for the current goal is (andEL ((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) (d ∈ rational_numbers) Hfour).

We prove the intermediate claim HdQ: d ∈ rational_numbers.

An exact proof term for the current goal is (andER ((a ∈ rational_numbers ∧ b ∈ rational_numbers) ∧ c ∈ rational_numbers) (d ∈ rational_numbers) Hfour).

We prove the intermediate claim Hab: a ∈ rational_numbers ∧ b ∈ rational_numbers.

An exact proof term for the current goal is (andEL (a ∈ rational_numbers ∧ b ∈ rational_numbers) (c ∈ rational_numbers) Hthree).

We prove the intermediate claim HcQ: c ∈ rational_numbers.

An exact proof term for the current goal is (andER (a ∈ rational_numbers ∧ b ∈ rational_numbers) (c ∈ rational_numbers) Hthree).

We prove the intermediate claim HaQ: a ∈ rational_numbers.

An exact proof term for the current goal is (andEL (a ∈ rational_numbers) (b ∈ rational_numbers) Hab).

We prove the intermediate claim HbQ: b ∈ rational_numbers.

An exact proof term for the current goal is (andER (a ∈ rational_numbers) (b ∈ rational_numbers) Hab).

We prove the intermediate claim HUinBx: open_interval a b ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (open_interval_in_rational_open_intervals_basis a b HaQ HbQ).

We prove the intermediate claim HVinBy: open_interval c d ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (open_interval_in_rational_open_intervals_basis c d HcQ HdQ).

We prove the intermediate claim HRepl: setprod (open_interval a b) (open_interval c d) ∈ {setprod (open_interval a b) V|V ∈ rational_open_intervals_basis}.

An exact proof term for the current goal is (ReplI rational_open_intervals_basis (λV : set ⇒ setprod (open_interval a b) V) (open_interval c d) HVinBy).

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

An exact proof term for the current goal is (famunionI rational_open_intervals_basis (λU : set ⇒ {setprod U V|V ∈ rational_open_intervals_basis}) (open_interval a b) (setprod (open_interval a b) (open_interval c d)) HUinBx HRepl).

Let r be given.

Assume Hr: r ∈ product_basis_from rational_open_intervals_basis rational_open_intervals_basis.

We will prove r ∈ rational_rectangle_basis.

We prove the intermediate claim HexU: ∃U ∈ rational_open_intervals_basis, r ∈ {setprod U V|V ∈ rational_open_intervals_basis}.

An exact proof term for the current goal is (famunionE rational_open_intervals_basis (λU : set ⇒ {setprod U V|V ∈ rational_open_intervals_basis}) r Hr).

Apply HexU to the current goal.

Let U be given.

Assume HUcore.

We prove the intermediate claim HU: U ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (andEL (U ∈ rational_open_intervals_basis) (r ∈ {setprod U V|V ∈ rational_open_intervals_basis}) HUcore).

We prove the intermediate claim HrRepl: r ∈ {setprod U V|V ∈ rational_open_intervals_basis}.

An exact proof term for the current goal is (andER (U ∈ rational_open_intervals_basis) (r ∈ {setprod U V|V ∈ rational_open_intervals_basis}) HUcore).

We prove the intermediate claim HexV: ∃V ∈ rational_open_intervals_basis, r = setprod U V.

An exact proof term for the current goal is (ReplE rational_open_intervals_basis (λV0 : set ⇒ setprod U V0) r HrRepl).

Apply HexV to the current goal.

Let V be given.

Assume HVcore.

We prove the intermediate claim HV: V ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (andEL (V ∈ rational_open_intervals_basis) (r = setprod U V) HVcore).

We prove the intermediate claim Hreq: r = setprod U V.

An exact proof term for the current goal is (andER (V ∈ rational_open_intervals_basis) (r = setprod U V) HVcore).

We prove the intermediate claim HexUab: ∃a, ∃b, (a ∈ rational_numbers ∧ b ∈ rational_numbers ∧ U = open_interval a b).

An exact proof term for the current goal is (rational_open_intervals_basisE U HU).

We prove the intermediate claim HexVcd: ∃c, ∃d, (c ∈ rational_numbers ∧ d ∈ rational_numbers ∧ V = open_interval c d).

An exact proof term for the current goal is (rational_open_intervals_basisE V HV).

Apply HexUab to the current goal.

Let a be given.

Assume Ha2.

Apply Ha2 to the current goal.

Let b be given.

Assume Hab.

Apply HexVcd to the current goal.

Let c be given.

Assume Hc2.

Apply Hc2 to the current goal.

Let d be given.

Assume Hcd.

We prove the intermediate claim HabLeft: a ∈ rational_numbers ∧ b ∈ rational_numbers.

An exact proof term for the current goal is (andEL (a ∈ rational_numbers ∧ b ∈ rational_numbers) (U = open_interval a b) Hab).

We prove the intermediate claim HUeq: U = open_interval a b.

An exact proof term for the current goal is (andER (a ∈ rational_numbers ∧ b ∈ rational_numbers) (U = open_interval a b) Hab).

We prove the intermediate claim HaQ: a ∈ rational_numbers.

An exact proof term for the current goal is (andEL (a ∈ rational_numbers) (b ∈ rational_numbers) HabLeft).

We prove the intermediate claim HbQ: b ∈ rational_numbers.

An exact proof term for the current goal is (andER (a ∈ rational_numbers) (b ∈ rational_numbers) HabLeft).

We prove the intermediate claim HcdLeft: c ∈ rational_numbers ∧ d ∈ rational_numbers.

An exact proof term for the current goal is (andEL (c ∈ rational_numbers ∧ d ∈ rational_numbers) (V = open_interval c d) Hcd).

We prove the intermediate claim HVeql: V = open_interval c d.

An exact proof term for the current goal is (andER (c ∈ rational_numbers ∧ d ∈ rational_numbers) (V = open_interval c d) Hcd).

We prove the intermediate claim HcQ: c ∈ rational_numbers.

An exact proof term for the current goal is (andEL (c ∈ rational_numbers) (d ∈ rational_numbers) HcdLeft).

We prove the intermediate claim HdQ: d ∈ rational_numbers.

An exact proof term for the current goal is (andER (c ∈ rational_numbers) (d ∈ rational_numbers) HcdLeft).

We prove the intermediate claim HUsubR: U ⊆ R.

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

An exact proof term for the current goal is (open_interval_Subq_R a b).

We prove the intermediate claim HVsubR: V ⊆ R.

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

An exact proof term for the current goal is (open_interval_Subq_R c d).

We prove the intermediate claim HrectSubRR: setprod U V ⊆ setprod R R.

An exact proof term for the current goal is (setprod_Subq U V R R HUsubR HVsubR).

We prove the intermediate claim HrectPow: setprod U V ∈ 𝒫 (setprod R R).

An exact proof term for the current goal is (PowerI (setprod R R) (setprod U V) HrectSubRR).

We prove the intermediate claim HexDef: ∃a0 b0 c0 d0 : set, a0 ∈ rational_numbers ∧ b0 ∈ rational_numbers ∧ c0 ∈ rational_numbers ∧ d0 ∈ rational_numbers ∧ setprod U V = setprod (open_interval a0 b0) (open_interval c0 d0).

We use a to witness the existential quantifier.

We use b to witness the existential quantifier.

We use c to witness the existential quantifier.

We use d to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaQ.

An exact proof term for the current goal is HbQ.

An exact proof term for the current goal is HcQ.

An exact proof term for the current goal is HdQ.

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

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

Use reflexivity.

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

An exact proof term for the current goal is (SepI (𝒫 (setprod R R)) (λr0 : set ⇒ ∃a0 b0 c0 d0 : set, a0 ∈ rational_numbers ∧ b0 ∈ rational_numbers ∧ c0 ∈ rational_numbers ∧ d0 ∈ rational_numbers ∧ r0 = setprod (open_interval a0 b0) (open_interval c0 d0)) (setprod U V) HrectPow HexDef).