Let U be given.

Assume HU: U ∈ generated_topology EuclidPlane circular_regions.

We will prove U ∈ generated_topology EuclidPlane rectangular_regions.

We prove the intermediate claim HUPow: U ∈ 𝒫 EuclidPlane.

An exact proof term for the current goal is (SepE1 (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ circular_regions, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ circular_regions, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ circular_regions, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUsub: U ⊆ EuclidPlane.

An exact proof term for the current goal is (PowerE EuclidPlane U HUPow).

We prove the intermediate claim HUrect: ∀x0 ∈ U, ∃r ∈ rectangular_regions, x0 ∈ r ∧ r ⊆ U.

Let x0 be given.

Assume Hx0U.

We prove the intermediate claim Hexb: ∃b ∈ circular_regions, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (HUprop x0 Hx0U).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim Hb: b ∈ circular_regions.

An exact proof term for the current goal is (andEL (b ∈ circular_regions) (x0 ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hbprop: x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ circular_regions) (x0 ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hx0b: x0 ∈ b.

An exact proof term for the current goal is (andEL (x0 ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (x0 ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim Hexr: ∃r ∈ rectangular_regions, x0 ∈ r ∧ r ⊆ b.

An exact proof term for the current goal is (rectangular_refines_circular_plane b Hb x0 Hx0b).

Apply Hexr to the current goal.

Let r be given.

Assume Hrpair.

We prove the intermediate claim Hr: r ∈ rectangular_regions.

An exact proof term for the current goal is (andEL (r ∈ rectangular_regions) (x0 ∈ r ∧ r ⊆ b) Hrpair).

We prove the intermediate claim Hrprop: x0 ∈ r ∧ r ⊆ b.

An exact proof term for the current goal is (andER (r ∈ rectangular_regions) (x0 ∈ r ∧ r ⊆ b) Hrpair).

We prove the intermediate claim Hx0r: x0 ∈ r.

An exact proof term for the current goal is (andEL (x0 ∈ r) (r ⊆ b) Hrprop).

We prove the intermediate claim Hrsubb: r ⊆ b.

An exact proof term for the current goal is (andER (x0 ∈ r) (r ⊆ b) Hrprop).

We prove the intermediate claim HrsubU: r ⊆ U.

An exact proof term for the current goal is (Subq_tra r b U Hrsubb HbsubU).

We use r to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hr.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0r.

An exact proof term for the current goal is HrsubU.

An exact proof term for the current goal is (SepI (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃r ∈ rectangular_regions, x0 ∈ r ∧ r ⊆ U0) U HUPow HUrect).

Let U be given.

Assume HU: U ∈ generated_topology EuclidPlane rectangular_regions.

We will prove U ∈ generated_topology EuclidPlane circular_regions.

We prove the intermediate claim HUPow: U ∈ 𝒫 EuclidPlane.

An exact proof term for the current goal is (SepE1 (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ rectangular_regions, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ rectangular_regions, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ rectangular_regions, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUcirc: ∀x0 ∈ U, ∃u ∈ circular_regions, x0 ∈ u ∧ u ⊆ U.

Let x0 be given.

Assume Hx0U.

We prove the intermediate claim Hexb: ∃b ∈ rectangular_regions, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (HUprop x0 Hx0U).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim Hb: b ∈ rectangular_regions.

An exact proof term for the current goal is (andEL (b ∈ rectangular_regions) (x0 ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hbprop: x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ rectangular_regions) (x0 ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hx0b: x0 ∈ b.

An exact proof term for the current goal is (andEL (x0 ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (x0 ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim Hexu: ∃u ∈ circular_regions, x0 ∈ u ∧ u ⊆ b.

An exact proof term for the current goal is (circular_refines_rectangular_plane b Hb x0 Hx0b).

Apply Hexu to the current goal.

Let u be given.

Assume Hupair.

We prove the intermediate claim Hu: u ∈ circular_regions.

An exact proof term for the current goal is (andEL (u ∈ circular_regions) (x0 ∈ u ∧ u ⊆ b) Hupair).

We prove the intermediate claim Huprop: x0 ∈ u ∧ u ⊆ b.

An exact proof term for the current goal is (andER (u ∈ circular_regions) (x0 ∈ u ∧ u ⊆ b) Hupair).

We prove the intermediate claim Hx0u: x0 ∈ u.

An exact proof term for the current goal is (andEL (x0 ∈ u) (u ⊆ b) Huprop).

We prove the intermediate claim Husubb: u ⊆ b.

An exact proof term for the current goal is (andER (x0 ∈ u) (u ⊆ b) Huprop).

We prove the intermediate claim HusubU: u ⊆ U.

An exact proof term for the current goal is (Subq_tra u b U Husubb HbsubU).

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hu.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0u.

An exact proof term for the current goal is HusubU.

An exact proof term for the current goal is (SepI (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ circular_regions, x0 ∈ b ∧ b ⊆ U0) U HUPow HUcirc).