Let U be given.
Assume HU: U ∈ rectangular_regions.
We will prove U ∈ R2_standard_topology.
We prove the intermediate claim Hdesc: ∃a b c d : set, a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U = {p ∈ EuclidPlane|∃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) (λ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}) U HU).
Apply Hdesc to the current goal.
Let a be given.
Assume Hbex: ∃b c d : set, a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.
Apply Hbex to the current goal.
Let b be given.
Assume Hcex: ∃c d : set, a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.
Apply Hcex to the current goal.
Let c be given.
Assume Hdex: ∃d : set, a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.
Apply Hdex to the current goal.
Let d be given.
Assume Hcore: a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}.
We prove the intermediate claim Hleft6: a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d) (U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}) Hcore).
We prove the intermediate claim HUeq: U = {p ∈ EuclidPlane|∃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 (andER (a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d) (U = {p ∈ EuclidPlane|∃x y : set, p = (x,y) ∧ Rlt a x ∧ Rlt x b ∧ Rlt c y ∧ Rlt y d}) Hcore).
We prove the intermediate claim Hleft5: a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b) (Rlt c d) Hleft6).
We prove the intermediate claim Hcd: Rlt c d.
An exact proof term for the current goal is (andER (a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b) (Rlt c d) Hleft6).
We prove the intermediate claim Hab: Rlt a b.
An exact proof term for the current goal is (andER (a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R) (Rlt a b) Hleft5).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (open_rectangle_in_R2_standard_topology a b c d Hab Hcd).
∎