The crosscut theorem for a general Jordan curve

P is a simple polygonal arc with distinct endpoints p, q on a Jordan curve C and all its remaining points in D = Int(C); A₁, A₂ are the two arcs of C from p to q. Then D ∖ P has exactly two components, namely Int(A₁ ∪ P) and Int(A₂ ∪ P), and consequently ℝ² ∖ (C ∪ P) has precisely three regions, with boundaries C, A₁ ∪ P, A₂ ∪ P.

The proof is short because both halves already exist. Schoenflies.crosscut_cells exhibits two distinct components of D ∖ P; Schoenflies.crosscut_components_exhaust says there are no others; and the final paragraph is Schoenflies.Plane.connectedComponentIn_eq_of_frontier_disjoint applied three times. All this module does is fit the pieces together and name the result.

The two sides are named by their arcs, and they are inside (Aᵢ ∪ P)

Everything Part II asks of this theorem is asked of one labelled side: lem:crosscut-side-correspondence wants "the component whose closure meets C in Aᵢ" as a function of i, and prop:initial-pair, lem:cellulation-invariants and thm:finite-transfer all consume the labelled form. So there is no existential anywhere in the conclusions below: the side belonging to the arc A is literally Schoenflies.inside (A ∪ P), which is already a function of A, carries the whole inside/IsSeparating API, and is exactly the set the blueprint writes Int(A ∪ P). The labelling lemma is IsCrosscut.closure_side_inter:

closure (inside (A₁ ∪ P)) ∩ C = A₁.

Each statement is proved for A₁ only; IsCutPair.symm swaps the two arcs, so h.foo hjordan hcut.symm is the A₂ instance of h.foo hjordan hcut. That is why no lemma below mentions A₂ in its conclusion.

What is assumed

Two hypotheses are threaded through, both of which are being discharged elsewhere right now:

• hjordan : ∀ S : Set Plane, IsJordanCurve S → IsSeparating S — thm:jordan. Only the separation clause is used; the boundary clause is part of Schoenflies.IsSeparating, so no second hypothesis is needed.
• hcollars : HasArcCollars (inside C) P — blueprint Lemma 1.8 (b) for the arc P inside the Jordan domain, the standing hypothesis of Schoenflies/CrosscutAtMostTwo.lean.

Neither is a restatement of anything proved here.

Blueprint

• Schoenflies.IsCrosscut — the hypotheses of thm:general-crosscut on C, P, p, q.
• Schoenflies.IsCutPair — "A₁, A₂ the two arcs of C from p to q, as in lem:jordan-circle"; Schoenflies.exists_isCutPair produces one from IsJordanCurve.two_arcs.
• Schoenflies.IsCrosscut.side_subset, .side_isComponent, .closure_side_inter, .side_ne, .disjoint_sides, .components_eq, .inside_diff_eq — the first half of thm:general-crosscut, one labelled side at a time, and then the exhaustion. The side's own topology comes with it: .isOpen_side, .isConnected_side, .isBounded_side, .side_nonempty, .frontier_side, .closure_side.
• Schoenflies.general_crosscut — thm:general-crosscut, first sentence, bundled.
• Schoenflies.IsCrosscut.compl_eq, .compl_eq_three, .outside_isComponent, .side_isComponent_compl, .three_regions — the "consequently" sentence.
• Schoenflies.general_crosscut_three_regions — thm:general-crosscut, second sentence, bundled, with the three boundaries.
• Schoenflies.IsArcBetween.not_subset_pair — an arc is more than its two endpoints; general, and the only new fact about arcs this module needs.

An arc is more than its two endpoints

This is what Schoenflies.arcs_ne needs in order to conclude A₁ ≠ A₂ from the fact that the two arcs meet only at p and q. It is a general fact about arcs and belongs in Schoenflies/Curve.lean; it is here because nothing on main states it.

theorem Schoenflies.IsArcBetween.not_subset_pair {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : ¬A ⊆ {p, q}

An arc between two points is not just those two points: the midpoint parameter carries a third point of it, because the parametrisation is injective.

The configuration

Two bundles of hypotheses. IsCrosscut C P p q is the blueprint's "P is a simple polygonal arc with distinct endpoints p, q ∈ C and all other points in D = Int(C)"; distinctness of p and q is not a field, since an arc between two points always has them distinct. IsCutPair C p q A₁ A₂ is "A₁, A₂ are the two arcs of C from p to q". The two are kept apart because the arcs are a choice — swapping them is a symmetry of the whole theorem, and IsCutPair.symm is what makes every statement below need proving only once.

structure Schoenflies.IsCrosscut (C P : Set Plane) (p q : Plane) : Prop

The crosscut configuration. A Jordan curve C and a simple polygonal arc P from p ∈ C to q ∈ C whose remaining points all lie in the Jordan domain inside C.

• curve : IsJordanCurve C

  C is a Jordan curve.

• arc : IsArcBetween P p q

  P is a simple arc from p to q.

• polygonal : IsPolygonal P

  P is polygonal.

• left_mem : p ∈ C

  The first endpoint is on the curve.

• right_mem : q ∈ C

  The second endpoint is on the curve.

• sdiff_subset : P \ {p, q} ⊆ inside C

  Every other point of the crosscut is inside the curve.

structure Schoenflies.IsCutPair (C : Set Plane) (p q : Plane) (A₁ A₂ : Set Plane) : Prop

The two arcs of C from p to q, as in lem:jordan-circle: two arcs between the same two points which cover the curve and meet in exactly those two points.

• fst : IsArcBetween A₁ p q

  The first piece is an arc from p to q.

• snd : IsArcBetween A₂ p q

  The second piece is an arc from p to q.

• union_eq : A₁ ∪ A₂ = C

  The two pieces cover the curve.

• inter_eq : A₁ ∩ A₂ = {p, q}

  The two pieces meet exactly at the two cut points.

theorem Schoenflies.IsCutPair.symm {C A₁ A₂ : Set Plane} {p q : Plane} (h : IsCutPair C p q A₁ A₂) : IsCutPair C p q A₂ A₁

Swapping the two arcs. Every conclusion of this module is proved for A₁ and obtained for A₂ by composing with this.

theorem Schoenflies.IsCutPair.fst_subset {C A₁ A₂ : Set Plane} {p q : Plane} (h : IsCutPair C p q A₁ A₂) : A₁ ⊆ C

theorem Schoenflies.IsCutPair.snd_subset {C A₁ A₂ : Set Plane} {p q : Plane} (h : IsCutPair C p q A₁ A₂) : A₂ ⊆ C

theorem Schoenflies.IsCutPair.ne {C A₁ A₂ : Set Plane} {p q : Plane} (h : IsCutPair C p q A₁ A₂) : A₁ ≠ A₂

The two arcs are distinct: they meet only at p and q, and neither is just {p, q}.

theorem Schoenflies.exists_isCutPair {C : Set Plane} {p q : Plane} (hC : IsJordanCurve C) (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ∃ (A₁ : Set Plane) (A₂ : Set Plane), IsCutPair C p q A₁ A₂

Two distinct points of a Jordan curve cut it into a pair of arcs. This is IsJordanCurve.two_arcs, repackaged.

Elementary consequences of the configuration

Nothing here needs thm:jordan: these are the set-theoretic facts that turn "the crosscut runs inside the curve" into the hypotheses Schoenflies.crosscut_cells takes.

theorem Schoenflies.IsCrosscut.left_notMem_inside {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : p ∉ inside C

theorem Schoenflies.IsCrosscut.right_notMem_inside {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : q ∉ inside C

theorem Schoenflies.IsCrosscut.inter_eq {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : P ∩ C = {p, q}

The crosscut meets the curve exactly at its two endpoints. Everything else on the crosscut is inside the curve, hence off it.

theorem Schoenflies.IsCrosscut.disjoint_outside {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : Disjoint P (outside C)

The crosscut misses the outside of the curve entirely: its endpoints are on the curve and everything else is inside. This is the sentence the three-region half opens with.

theorem Schoenflies.IsCrosscut.inter_subset_arc {C P A₁ A₂ : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : P ∩ C ⊆ A₁

P ∩ C ⊆ A₁: the crosscut meets the curve only in the two points that lie on both arcs. This is the hypothesis hP₁ of Schoenflies.crosscut_cells.

theorem Schoenflies.IsCrosscut.arc_union_inter {C P A₁ A₂ : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : (A₁ ∪ P) ∩ C = A₁

(A₁ ∪ P) ∩ C = A₁: the curve J₁ of the blueprint meets C exactly in the arc it was built from. This is what turns clause (c) of Schoenflies.crosscut_cells into the labelling lemma.

theorem Schoenflies.IsCrosscut.isJordanCurve_union {C P A₁ A₂ : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : IsJordanCurve (A₁ ∪ P)

J₁ = A₁ ∪ P is a Jordan curve. The arc and the crosscut are two arcs from p to q meeting only at those two points.

The two separating curves, and where the outside of C sits

This is the paragraph of the blueprint proof that pins the roles of Wᵢ and Vᵢ: Ω† = Ext(C) is connected, unbounded and disjoint from Jᵢ, hence lies in Ext(Jᵢ).

theorem Schoenflies.IsCrosscut.isSeparating_curve {C P : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) : IsSeparating C

theorem Schoenflies.IsCrosscut.isSeparating_union {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : IsSeparating (A₁ ∪ P)

theorem Schoenflies.IsCrosscut.outside_subset_outside_union {C P A : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hA : A ⊆ C) : outside C ⊆ outside (A ∪ P)

Ext(C) ⊆ Ext(A ∪ P). The outside of C is connected and misses A ∪ P, so it lies in one component of the complement of A ∪ P; being unbounded, that component is unbounded, which is what Schoenflies.outside records.

Stated for an arbitrary A ⊆ C, since that is all the argument uses.

theorem Schoenflies.IsCrosscut.isRegionPair_curve (C : Set Plane) : IsRegionPair C (inside C) (outside C)

The pair (Ext(C), Int(C)) in the shape Schoenflies.crosscut_cells takes for (Ω, Ω'), with Ω = Int(C) the region the crosscut runs in.

theorem Schoenflies.IsCrosscut.isRegionPair_union (J : Set Plane) : IsRegionPair J (outside J) (inside J)

The pair (Wᵢ, Vᵢ) = (Ext(Jᵢ), Int(Jᵢ)).

The first half: Int(A₁ ∪ P) is a component of Int(C) ∖ P with closure meeting C

in A₁

Three applications of Schoenflies.crosscut_cells, one clause each. Everything is stated for the arc A₁; IsCutPair.symm supplies the A₂ instance.

theorem Schoenflies.IsCrosscut.side_subset {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : inside (A₁ ∪ P) ⊆ inside C \ P

Int(A₁ ∪ P) ⊆ Int(C) ∖ P. Clause (a) of lem:crosscut-cells, first half.

theorem Schoenflies.IsCrosscut.side_isComponent {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (z : Plane) : z ∈ inside (A₁ ∪ P) → connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P)

Int(A₁ ∪ P) is a connected component of Int(C) ∖ P. Clause (a) of lem:crosscut-cells.

theorem Schoenflies.IsCrosscut.closure_side_inter {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : closure (inside (A₁ ∪ P)) ∩ C = A₁

The labelling lemma: the closure of the side meets C exactly in its own arc. Clause (c) of lem:crosscut-cells. This is what makes A ↦ inside (A ∪ P) the correspondence lem:crosscut-side-correspondence asks for, and it is what distinguishes the two sides.

theorem Schoenflies.IsCrosscut.side_ne {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : inside (A₁ ∪ P) ≠ inside (A₂ ∪ P)

The two sides are distinct. Equal sides would have equal closures, hence equal arcs.

theorem Schoenflies.IsCrosscut.side_nonempty {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : (inside (A₁ ∪ P)).Nonempty

theorem Schoenflies.IsCrosscut.isOpen_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : IsOpen (inside (A₁ ∪ P))

theorem Schoenflies.IsCrosscut.isConnected_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : IsConnected (inside (A₁ ∪ P))

theorem Schoenflies.IsCrosscut.isBounded_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : Bornology.IsBounded (inside (A₁ ∪ P))

theorem Schoenflies.IsCrosscut.frontier_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : frontier (inside (A₁ ∪ P)) = A₁ ∪ P

The boundary of the side is its own Jordan curve A₁ ∪ P.

theorem Schoenflies.IsCrosscut.closure_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : closure (inside (A₁ ∪ P)) = inside (A₁ ∪ P) ∪ (A₁ ∪ P)

The closure of the side is the side together with its boundary curve. Paired with closure_side_inter this is the form lem:crosscut-side-correspondence reads the closure in.

theorem Schoenflies.IsCrosscut.disjoint_sides {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P))

The two sides are disjoint: they are distinct components of the same set.

The second half: there are no other components

Schoenflies.crosscut_components_exhaust applied to the two sides, which the previous section has just shown to be distinct components.

theorem Schoenflies.IsCrosscut.components_eq {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) (z : Plane) : z ∈ inside C \ P → connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P) ∨ connectedComponentIn (inside C \ P) z = inside (A₂ ∪ P)

Every component of Int(C) ∖ P is one of the two sides. This is the "at most two" half, lem:crosscut-at-most-two, applied to the two components lem:crosscut-cells produced.

theorem Schoenflies.IsCrosscut.inside_diff_eq {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : inside C \ P = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P)

Int(C) ∖ P is the disjoint union of the two sides.

theorem Schoenflies.general_crosscut {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : inside C \ P = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ (inside (A₁ ∪ P)).Nonempty ∧ (inside (A₂ ∪ P)).Nonempty ∧ inside (A₁ ∪ P) ≠ inside (A₂ ∪ P) ∧ (∀ z ∈ inside (A₁ ∪ P), connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P)) ∧ (∀ z ∈ inside (A₂ ∪ P), connectedComponentIn (inside C \ P) z = inside (A₂ ∪ P)) ∧ (∀ z ∈ inside C \ P, connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P) ∨ connectedComponentIn (inside C \ P) z = inside (A₂ ∪ P)) ∧ closure (inside (A₁ ∪ P)) ∩ C = A₁ ∧ closure (inside (A₂ ∪ P)) ∩ C = A₂

Theorem "Crosscut theorem", first sentence (thm:general-crosscut). Int(C) ∖ P has exactly two components, namely Int(A₁ ∪ P) and Int(A₂ ∪ P).

"Exactly two" is spelled out: the two sets are nonempty, disjoint, each is a component, they cover, they are distinct, and every component is one of them. The last two clauses are the labelling closure (inside (Aᵢ ∪ P)) ∩ C = Aᵢ, which is what tells the two apart. Each clause is separately available as a lemma in the Schoenflies.IsCrosscut namespace; this bundle exists only so that the blueprint statement appears once, in one place.

The three regions of ℝ² ∖ (C ∪ P)

The blueprint's final paragraph. P misses Ext(C), so the complement of C ∪ P splits as Ext(C) ⊔ (Int(C) ∖ P); the first half has just split the second summand in two; and each of the three pieces is a component of the whole because its boundary misses it (lem:clopen-component, here Schoenflies.Plane.connectedComponentIn_eq_of_frontier_disjoint).

theorem Schoenflies.IsCrosscut.compl_eq {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : (C ∪ P)ᶜ = outside C ∪ inside C \ P

ℝ² ∖ (C ∪ P) = Ext(C) ⊔ (Int(C) ∖ P). The crosscut lies wholly in C ∪ Int(C), so removing it from the complement of C costs the outside nothing.

theorem Schoenflies.IsCrosscut.compl_eq_three {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : (C ∪ P)ᶜ = outside C ∪ inside (A₁ ∪ P) ∪ inside (A₂ ∪ P)

ℝ² ∖ (C ∪ P) = Ext(C) ⊔ Int(A₁ ∪ P) ⊔ Int(A₂ ∪ P): the three regions, as sets.

theorem Schoenflies.IsCrosscut.outside_subset_compl {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : outside C ⊆ (C ∪ P)ᶜ

theorem Schoenflies.IsCrosscut.side_subset_compl {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : inside (A₁ ∪ P) ⊆ (C ∪ P)ᶜ

theorem Schoenflies.IsCrosscut.outside_isComponent {C P : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (z : Plane) : z ∈ outside C → connectedComponentIn (C ∪ P)ᶜ z = outside C

Ext(C) is a region of ℝ² ∖ (C ∪ P). Its boundary is C, which misses that open set; lem:clopen-component does the rest.

theorem Schoenflies.IsCrosscut.side_isComponent_compl {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (z : Plane) : z ∈ inside (A₁ ∪ P) → connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P)

Int(A₁ ∪ P) is a region of ℝ² ∖ (C ∪ P). Its boundary is A₁ ∪ P ⊆ C ∪ P, which misses that open set.

theorem Schoenflies.IsCrosscut.three_regions {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) (z : Plane) : z ∈ (C ∪ P)ᶜ → connectedComponentIn (C ∪ P)ᶜ z = outside C ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P) ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₂ ∪ P)

Every region of ℝ² ∖ (C ∪ P) is one of the three.

theorem Schoenflies.IsCrosscut.disjoint_outside_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : Disjoint (outside C) (inside (A₁ ∪ P))

The outside of C is disjoint from either side, since the sides lie inside C.

theorem Schoenflies.IsCrosscut.outside_ne_side {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : outside C ≠ inside (A₁ ∪ P)

The outside of C is not a side: it is unbounded and every side is bounded.

theorem Schoenflies.general_crosscut_three_regions {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : (C ∪ P)ᶜ = outside C ∪ inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∧ (∀ z ∈ outside C, connectedComponentIn (C ∪ P)ᶜ z = outside C) ∧ (∀ z ∈ inside (A₁ ∪ P), connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P)) ∧ (∀ z ∈ inside (A₂ ∪ P), connectedComponentIn (C ∪ P)ᶜ z = inside (A₂ ∪ P)) ∧ (∀ z ∈ (C ∪ P)ᶜ, connectedComponentIn (C ∪ P)ᶜ z = outside C ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P) ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₂ ∪ P)) ∧ Disjoint (outside C) (inside (A₁ ∪ P)) ∧ Disjoint (outside C) (inside (A₂ ∪ P)) ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ outside C ≠ inside (A₁ ∪ P) ∧ outside C ≠ inside (A₂ ∪ P) ∧ inside (A₁ ∪ P) ≠ inside (A₂ ∪ P) ∧ frontier (outside C) = C ∧ frontier (inside (A₁ ∪ P)) = A₁ ∪ P ∧ frontier (inside (A₂ ∪ P)) = A₂ ∪ P

Theorem "Crosscut theorem", second sentence (thm:general-crosscut). ℝ² ∖ (C ∪ P) has precisely three regions, whose boundaries are C, A₁ ∪ P and A₂ ∪ P.

The three are named: Ext(C), Int(A₁ ∪ P), Int(A₂ ∪ P). They cover, they are pairwise disjoint and pairwise distinct, each is a component, every component is one of them, and the three boundaries are as stated. "Pairwise distinct" is what makes this three regions and not fewer; it is not a consequence of the covering, so it is a clause here.