Let a, b, c and d be given.
Assume Ha Hb Hc Hd Hab Hcd.
We will prove {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d} ∈ rectangular_regions.
We prove the intermediate claim HPow: {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d} ∈ 𝒫 EuclidPlane.
Apply PowerI EuclidPlane {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d} to the current goal.
Let p be given.
Assume Hp.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ ∃x y : set, p0 = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d) p Hp).
We prove the intermediate claim HPred: ∃a0 b0 c0 d0 : set, a0 ∈ R ∧ b0 ∈ R ∧ c0 ∈ R ∧ d0 ∈ R ∧ Rlt a0 b0 ∧ Rlt c0 d0 ∧ {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d} = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a0 x ∧ Rlt x b0 ∧ Rlt c0 y ∧ Rlt y 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.
Apply and6I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is Hc.
An exact proof term for the current goal is Hd.
An exact proof term for the current goal is Hab.
An exact proof term for the current goal is Hcd.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 EuclidPlane) (λU0 : set ⇒ ∃a0 b0 c0 d0 : set, a0 ∈ R ∧ b0 ∈ R ∧ c0 ∈ R ∧ d0 ∈ R ∧ Rlt a0 b0 ∧ Rlt c0 d0 ∧ U0 = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a0 x ∧ Rlt x b0 ∧ Rlt c0 y ∧ Rlt y d0}) {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d} HPow HPred).
∎