Let p be given.

Assume Hp: p ∈ {p0 ∈ EuclidPlane|∃x y : set, p0 = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.

We will prove p ∈ rectangle_set (open_interval a b) (open_interval c d).

We prove the intermediate claim Hex: ∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d.

An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ ∃x y : set, p0 = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d) p Hp).

Apply Hex to the current goal.

Let x be given.

Assume Hexy: ∃y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d.

Apply Hexy to the current goal.

Let y be given.

Assume Hcore: p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d.

We prove the intermediate claim Hleft4: p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y.

An exact proof term for the current goal is (andEL (p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y) (Rlt y d) Hcore).

We prove the intermediate claim Hyd: Rlt y d.

An exact proof term for the current goal is (andER (p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y) (Rlt y d) Hcore).

We prove the intermediate claim Hleft3: p = (x,y) ∧ Rlt a x ∧ Rlt x b.

An exact proof term for the current goal is (andEL (p = (x,y) ∧ Rlt a x ∧ Rlt x b) (Rlt c y) Hleft4).

We prove the intermediate claim Hcy: Rlt c y.

An exact proof term for the current goal is (andER (p = (x,y) ∧ Rlt a x ∧ Rlt x b) (Rlt c y) Hleft4).

We prove the intermediate claim Hleft2: p = (x,y) ∧ Rlt a x.

An exact proof term for the current goal is (andEL (p = (x,y) ∧ Rlt a x) (Rlt x b) Hleft3).

We prove the intermediate claim Hxb: Rlt x b.

An exact proof term for the current goal is (andER (p = (x,y) ∧ Rlt a x) (Rlt x b) Hleft3).

We prove the intermediate claim Hpeq: p = (x,y).

An exact proof term for the current goal is (andEL (p = (x,y)) (Rlt a x) Hleft2).

We prove the intermediate claim Hax: Rlt a x.

An exact proof term for the current goal is (andER (p = (x,y)) (Rlt a x) Hleft2).

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (RltE_right a x Hax).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (RltE_right c y Hcy).

We prove the intermediate claim HxIn: x ∈ open_interval a b.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a z ∧ Rlt z b) x HxR (andI (Rlt a x) (Rlt x b) Hax Hxb)).

We prove the intermediate claim HyIn: y ∈ open_interval c d.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) y HyR (andI (Rlt c y) (Rlt y d) Hcy Hyd)).

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

An exact proof term for the current goal is (tuple_2_rectangle_set (open_interval a b) (open_interval c d) x y HxIn HyIn).

Let p be given.

Assume Hp: p ∈ rectangle_set (open_interval a b) (open_interval c d).

We will prove p ∈ {p0 ∈ EuclidPlane|∃x y : set, p0 = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.

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).

We prove the intermediate claim HpE: p ∈ EuclidPlane.

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).

We prove the intermediate claim Hp0ineq: Rlt a (p 0) ∧ Rlt (p 0) b.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z ∧ Rlt z b) (p 0) Hp0U).

We prove the intermediate claim Hp1ineq: Rlt c (p 1) ∧ Rlt (p 1) d.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt c z ∧ Rlt z d) (p 1) Hp1V).

We prove the intermediate claim Hap0: Rlt a (p 0).

An exact proof term for the current goal is (andEL (Rlt a (p 0)) (Rlt (p 0) b) Hp0ineq).

We prove the intermediate claim Hp0b: Rlt (p 0) b.

An exact proof term for the current goal is (andER (Rlt a (p 0)) (Rlt (p 0) b) Hp0ineq).

We prove the intermediate claim Hcp1: Rlt c (p 1).

An exact proof term for the current goal is (andEL (Rlt c (p 1)) (Rlt (p 1) d) Hp1ineq).

We prove the intermediate claim Hp1d: Rlt (p 1) d.

An exact proof term for the current goal is (andER (Rlt c (p 1)) (Rlt (p 1) d) Hp1ineq).

We prove the intermediate claim Hpred: ∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d.

We use (p 0) to witness the existential quantifier.

We use (p 1) to witness the existential quantifier.

Apply and5I to the current goal.

An exact proof term for the current goal is HpEta.

An exact proof term for the current goal is Hap0.

An exact proof term for the current goal is Hp0b.

An exact proof term for the current goal is Hcp1.

An exact proof term for the current goal is Hp1d.

An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ ∃x y : set, p0 = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d) p HpE Hpred).