Connectivity for betweenness

Used interfaces
Imports
Interface:Collinearity
Exports
Interface:Connectivity for betweenness

This is part of a series of modules which prove a variety of geometrical theorems starting with Tarski's axioms for geometry. We follow the formalization of Julien Narboux which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.

This page is devoted to the proof of one theorem, A ≠ B ∧ between A B C ∧ between A B D → between A C D ∨ between A D C. This is called outer connectivity for betweenness by Narboux and Givant. It was once considered an axiom of Tarski's system, but was proved from the other axioms by Gupta in 1965

The proof is not simple; Givant calls it "rather involved" and Narboux devotes two and a half pages to an informal proof (and an explanation of part of the formal proof).

We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:

import (CLASSICAL Interface:Classical_propositional_calculus () ())
import (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())
import (START Interface:Collinearity (CLASSICAL FIRSTORDER) ())

var (point A B C D E P Q R A′ B′ C′ D′ B″ C″)
var (variable a b b′ c c′ d′ e p q r b″ c″)

Summary

construction of C′, D′, B′, and B″

Here's an outline of the proof, illustrating which points we construct but leaving most of the detailed line segment congruences for the detailed formal proof.

We first construct C′ and D′ extending the line segments A D and A C by a distance of C D in both cases. Eventually, the proof will show that C = C′ or D = D′.

Then extend the line segments A C′ and A D′ to points B′ and B″ by distances of C B and D B. The result of this construction is that the distance from B is the same to either B′ or B″ and thus we can conclude that B′ = B″.

construction of E

The point E lies at the intersection of C C′ and D D′.

At this point we assume C ≠ C′ and will deduce from that D = D′.

construction of P, Q, and R

Extend C′ C by the distance C D′ to a point P. Extend D′ C by the distance C E to a point R. Extend P R by the distance R P to a point Q.

D′ D ≡ P Q and C P ≡ C Q

By some congruences we can show first D′ D ≡ P Q, which we'll need at the end of the proof, and C P ≡ C Q, which leads to the next step.

B P ≡ B Q and B′ P ≡ B′ Q

C′ P ≡ C′ Q

At this point we will apply EquidistantLine five times. In every case we will show that x P ≡ x Q (based on two such existing congruences). For the starting point, we already have C P ≡ C Q and R P ≡ R Q. In turn, we will prove a similar congruence for D′, B, B′, and C′. Those cases easily fit the pictures we have been drawing so far. But we don't stop there: because C′, C, and P are collinear, we can also conclude P P ≡ P Q (this last one doesn't quite as readily lend itself to being illustrated in diagram form, but the first four are illustrated in the adjacent figures).

Of course, P P ≡ P Q implies P = Q, which in turn implies D = D′ (via D D′ ≡ P Q).

We have shown that C ≠ C′ implies D = D′, or in other words C = C′ ∨ D = D′. The former implies A D C and the latter implies A C D, so we reach the conclusion that between A C D ∨ between A D C.

Construction of C′, D′, B′, and B″

construction of C′, D′, B′, and B″

We construct c′ such that between A D c′ ∧ D c′ ≡ C D and d′ such that between A C d′ ∧ C d′ ≡ C D.

Then we construct b′ such that between A c′ b′ ∧ c′ b′ ≡ C B and b″ such that between A d′ b″ ∧ d′ b″ ≡ D B.

The following lemma embodies these constructions, and a bit of rearrangement of the quantifiers.

thm (BetweennessOuterConnectivity-cdbb
  ((A c′ d′ b′ b″) (B c′ d′ b′ b″) (C c′ d′ b′ b″) (D c′ d′ b′ b″)) ()
  ((((A ≠ B) ∧ (between A B C)) ∧ (between A B D)) →
    (∃ c′ (∃ d′ (∃ b′ (∃ b″
      ((((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
      ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
      ((between A (value c′) (value b′)) ∧ ((value c′) (value b′) ≡ C B))) ∧
      ((between A (value d′) (value b″)) ∧ ((value d′) (value b″) ≡ D B))) ∧
      (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))))))) (
        c′ A D C D SegmentConstruction
        d′ A C C D SegmentConstruction
        introduceConjunction

        c′ d′ ((between A D (value c′)) ∧ (D (value c′) ≡ C D))
          ((between A C (value d′)) ∧ (C (value d′) ≡ C D))
          ThereExistsScattering
        eliminateBiconditionalForward

        applyModusPonens

So far we have the construction of c′ and d′, specifically ∃ c′ ∃ d′ ((between A D c′ ∧ D c′ ≡ C D) ∧ (between A C d′ ∧ C d′ ≡ C D)). We now turn to b′.

        b′ A (value c′) C B SegmentConstruction
        d′ generalize
        c′ generalize

        combineThereExistsForAll

        d′
          (((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D)))
          (∃ b′ ((between A (value c′) (value b′))
            ∧ ((value c′) (value b′) ≡ C B)))
          ThereExistsConjunctionRightCombining
        c′ addThereExists
        applyModusPonens

That gives us ∃ c′ ∃ d′ ((between A D c′ ∧ D c′ ≡ C D) ∧ (between A C d′ ∧ C d′ ≡ C D) ∧ ∃ b′ (between A c′ b′ ∧ c′ b′ ≡ C B)). The next step is to move ∃ b′ to the front.

        b′
          (((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D)))
          ((between A (value c′) (value b′))
            ∧ ((value c′) (value b′) ≡ C B))
          ThereExistsConjunctionMovement
        eliminateBiconditionalForward
        d′ addThereExists
        c′ addThereExists
        applyModusPonens

Now we construct b″, which starts with ∃ b″ (between A d′ b″ ∧ d′ b″ ≡ D B) and then moves the quantifiers to the front.

        b″ A (value d′) D B SegmentConstruction
        d′ generalize

        introduceConjunction

        c′
          (∃ d′ (∃ b′
            ((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
              ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
              ((between A (value c′) (value b′))
                ∧ ((value c′) (value b′) ≡ C B)))
          ))
          (∀ d′ (∃ b″ ((between A (value d′) (value b″)) ∧ ((value d′) (value b″) ≡ D B))))
          ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        applyModusPonens

        d′
          (∃ b′
            ((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
              ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
              ((between A (value c′) (value b′))
                ∧ ((value c′) (value b′) ≡ C B)))
          )
          (∃ b″ ((between A (value d′) (value b″)) ∧ ((value d′) (value b″) ≡ D B)))
          ThereExistsConjunctionRightCombining
        c′ addThereExists
        applyModusPonens

        b′ b″
          ((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
            ((between A (value c′) (value b′))
              ∧ ((value c′) (value b′) ≡ C B)))
          ((between A (value d′) (value b″)) ∧ ((value d′) (value b″) ≡ D B))
          ThereExistsScattering
        eliminateBiconditionalForward
        d′ addThereExists
        c′ addThereExists
        applyModusPonens

Now we need to add in A ≠ B ∧ between A B C ∧ between A B D, and move it inside all four quantifiers.

        (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)) introduceAntecedent

        (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)) ImplicationReflexivity
        composeConjunction

        c′
          (∃ d′ (∃ b′ (∃ b″
            (((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
            ((between A (value c′) (value b′))
              ∧ ((value c′) (value b′) ≡ C B))) ∧
            ((between A (value d′) (value b″))
              ∧ ((value d′) (value b″) ≡ D B)))
          )))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
        ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        applySyllogism

        d′
          (∃ b′ (∃ b″
            (((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
            ((between A (value c′) (value b′))
              ∧ ((value c′) (value b′) ≡ C B))) ∧
            ((between A (value d′) (value b″))
              ∧ ((value d′) (value b″) ≡ D B)))
          ))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
        ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        c′ addThereExists
        applySyllogism

        b′
          (∃ b″
            (((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
            ((between A (value c′) (value b′))
              ∧ ((value c′) (value b′) ≡ C B))) ∧
            ((between A (value d′) (value b″))
              ∧ ((value d′) (value b″) ≡ D B)))
          )
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
        ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        d′ addThereExists
        c′ addThereExists
        applySyllogism

        b″
          (((((between A D (value c′)) ∧ (D (value c′) ≡ C D)) ∧
            ((between A C (value d′)) ∧ (C (value d′) ≡ C D))) ∧
            ((between A (value c′) (value b′))
              ∧ ((value c′) (value b′) ≡ C B))) ∧
            ((between A (value d′) (value b″))
              ∧ ((value d′) (value b″) ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
        ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        b′ addThereExists
        d′ addThereExists
        c′ addThereExists
        applySyllogism
))

B′ is equal to B″

B′ = B″

In this section we'll show that B′ = B″. The idea of the proof is simple: to get from B to B′ we go through D and C′, and to get from B to B″ we go through C and D′. As can be seen from the way we constructed the points, the three segments in the one case are congruent to the three segments in the other (although in reverse order), so the distance from B to either B′ or B″ is the same. Because A ≠ B, this implies that B′ = B″ by the uniqueness of segment construction (applied to A B B′ and A B B″).

B C′ ≡ B″ C

B C′ ≡ B″ C

Here we prove B C′ ≡ B″ C, starting with a few lemmas which we'll need.

thm (b-d-cprime
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B D C′)) (

First is between A B D.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionLeftElimination
        eliminateLeftConjunctInConsequent

Second is between A D C′

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent


        composeConjunction

The result follows from transitivity.

        A B D C′ BetweennessInnerTransitivityFlipped
        applySyllogism
))

thm (bdoubleprime-dprime-c
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B″ D′ C)) (

This is another application of transitivity, starting with between B″ D′ A.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D′ B″ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

The other thing we need is between D′ C A.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        A C D′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        B″ D′ A C BetweennessInnerTransitivity
        applySyllogism
))

thm (d-cprime-dprime-c
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (D C′ ≡ D′ C)) (

Each of the segments D C′ and D′ C is congruent to C D, so we just need to apply symmetry and transitivity.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        D C′ C D C D′ CongruenceTransitivity
        applySyllogism

        D C′ C D′ CongruenceRightCommutativity
        eliminateBiconditionalReverse
        applySyllogism
))

thm (b-cprime-bdoubleprime-c
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (B C′ ≡ B″ C)) (

We prove this theorem by applying OuterThreeSegment to B D C′ and B″ D′ C. The first step is between B D C′.

        A D C′ C D′ B′ B B″ b-d-cprime

The next is between B″ D′ C.

        A D C′ C D′ B′ B B″ bdoubleprime-dprime-c
        composeConjunction

The next is B D ≡ B″ D′.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        D′ B″ D B CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        D B D′ B″ CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

The last is D C′ D′ C

        A D C′ C D′ B′ B B″ d-cprime-dprime-c
        composeConjunction

Three segment gives us B C′ B″ C, the desired result.

        B D C′ B″ D′ C OuterThreeSegment
        applySyllogism
))

B B′ ≡ B″ B

B B′ ≡ B″ B

Here we extend the congruence from the previous section one more point. This is also an application of OuterThreeSegment, and we again break out some of the pieces into lemmas.

thm (a-b-cprime
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between A B C′)) (

This is an application of transitivity to between A B D

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionLeftElimination
        eliminateLeftConjunctInConsequent

and between A D C′.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

        A B D C′ BetweennessMiddleTransitivityFlipped
        applySyllogism
))

thm (b-cprime-bprime
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B C′ B′)) (

Here we apply transitivity to between A B C′.

        A D C′ C D′ B′ B B″ a-b-cprime

and between A C′ B′.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

        A B C′ B′ BetweennessInnerTransitivityFlipped
        applySyllogism
))

thm (a-c-bdoubleprime
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between A C B″)) (

Here we apply transitivity to between A C D′

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

and between A D′ B″

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

        A C D′ B″ BetweennessMiddleTransitivityFlipped
        applySyllogism
))

thm (bdoubleprime-c-b
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B″ C B)) (

Here we apply transitivity to A B C

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

and the previous lemma (between A C B″)

        A D C′ C D′ B′ B B″ a-c-bdoubleprime
        composeConjunction

to produce B C B″. Then we just need to switch the order of the endpoints.

        A B C B″ BetweennessInnerTransitivityFlipped
        applySyllogism

        B C B″ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism
))

thm (b-bprime-bdoubleprime-b
  () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (B B′ ≡ B″ B)) (

First we need between B C′ B′.

        A D C′ C D′ B′ B B″ b-cprime-bprime

Next we need between B″ C B.

        A D C′ C D′ B′ B B″ bdoubleprime-c-b
        composeConjunction

B C′ ≡ B″ C:

        A D C′ C D′ B′ B B″ b-cprime-bdoubleprime-c
        composeConjunction

C′ B′ ≡ C B:

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        composeConjunction

        B C′ B′ B″ C B OuterThreeSegment
        applySyllogism
))

B″ = B′

In this section we apply SegmentConstructionUniqueness to prove that B′ and B″ are in fact the same point. We start with some more betweenness transitivity lemmas.

thm (a-b-dprime () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between A B D′)) (

between A B C:

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

between A C D′:

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

        A B C D′ BetweennessMiddleTransitivityFlipped
        applySyllogism
))

thm (bdoubleprime-bprime () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (B″ = B′)) (

We'll prove B′ = B″ (and flip the order later). We first need A ≠ B.

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

Next is between A B B′, which follows from between A B C′ and between A C′ B′ by betweenness transitivity.

        A D C′ C D′ B′ B B″ a-b-cprime

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent
        composeConjunction

        A B C′ B′ BetweennessMiddleTransitivityFlipped
        applySyllogism

        composeConjunction

Next is between B B′ ≡ B″ B.

        A D C′ C D′ B′ B B″ b-bprime-bdoubleprime-b
        composeConjunction

Next is between A B B″, which follows from between A B D′ and between A D′ B″ by betweenness transitivity.

        A D C′ C D′ B′ B B″ a-b-dprime

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent
        composeConjunction

        A B D′ B″ BetweennessMiddleTransitivityFlipped
        applySyllogism

        composeConjunction

Finally we need B B″ ≡ B″ B.

        B B″ CongruenceABBA

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          introduceAntecedent
        composeConjunction

Applying segment construction uniqueness, and then flipping the order of the equality, we are done.

        A B B′ B″ B B″ SegmentConstructionUniqueness
        applySyllogism

        B′ B″ EqualitySymmetry
        eliminateBiconditionalReverse
        applySyllogism
))

Construction of E

C′ D′ ≡ C D, construction of E, E C ≡ E C′, and E D ≡ E D′

In this section we construct the point E and also prove a number of congruences. First (even before we construct E), we can apply outer five segment to the line segments B C D′ and B′ C′ D with points C′ and C to give us C′ D′ ≡ C D. Then we construct E as the intersection of C C′ and D D′ (the axiom of Pasch ensures its existence).

The congruences E C ≡ E C′ and E D ≡ E D′ may remind us of the familiar theorem that the diagonals of a rhombus bisect each other, but of course to say it that way would get ahead of ourselves. We can readily prove each of those two congruences, however, from a simple invocation of inner five segment.

C′ D′ ≡ C D

C′ D′ ≡ C D

We just said that this follows from inner five segment, but that's a slight oversimplification. That's true for the B ≠ C case (which we'll prove first), but there's a separate B = C case. We'll start with the B ≠ C case, and before the case itself we'll prove a few lemmas which represent the various antecedents of OuterFiveSegment.

thm (b-c-dprime () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B C D′)) (

We prove this via betweenness transitivity from between B C B″

        A D C′ C D′ B′ B B″ bdoubleprime-c-b

        B″ C B BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

and between C D′ B″.

        A D C′ C D′ B′ B B″ bdoubleprime-dprime-c

        B″ D′ C BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        B C B″ D′ BetweennessInnerTransitivity
        applySyllogism
))

thm (bprime-cprime-d () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (between B′ C′ D)) (

This follows by betweenness transitivity from B′ C′ B

        A D C′ C D′ B′ B B″ b-cprime-bprime

        B C′ B′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

and C′ D B

        A D C′ C D′ B′ B B″ b-d-cprime

        B D C′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        B′ C′ B D BetweennessInnerTransitivity
        applySyllogism
))

The next two lemmas just apply a substitution to turn B C′ ≡ B″ C, which we have already proved, into B C′ ≡ B′ C.

thm (b-cprime-bprime-c-lemma () ()
  (((B″ = B′) ∧ (B C′ ≡ B″ C)) → (B C′ ≡ B′ C)) (
        B EqualityReflexivity
        C′ EqualityReflexivity
        C EqualityReflexivity
        B B C′ C′ B″ B′ C C CongruenceBuilder
        detach2of2
        detach2of3
        detach1of2

        eliminateBiconditionalReverseInConsequent

        import
))

thm (b-cprime-bprime-c () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (B C′ ≡ B′ C)) (
        A D C′ C D′ B′ B B″ bdoubleprime-bprime
        A D C′ C D′ B′ B B″ b-cprime-bdoubleprime-c
        composeConjunction

        B″ B′ B C′ C b-cprime-bprime-c-lemma
        applySyllogism
))

thm (cprime-dprime-c-d-case-bnotc () ()
  (((B ≠ C) ∧
    ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))) →
  (C′ D′ ≡ C D)) (

For outer five segment, we first need B ≠ C.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionRightElimination

Next is between B C D′.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ b-c-dprime
        applySyllogism

        composeConjunction

Next is between B′ C′ D.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ bprime-cprime-d
        applySyllogism

        composeConjunction

Next is B C ≡ B′ C′.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C′ B′ C B CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        C B C′ B′ CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Next is C D′ ≡ C′ D.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

        D C′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        C D D C′ CongruenceRightCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        C D′ C D C′ D CongruenceTransitivity
        applySyllogism

        composeConjunction

Next is B C′ ≡ B′ C.

        (B ≠ C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ b-cprime-bprime-c
        applySyllogism

        composeConjunction

Last is C C′ ≡ C′ C.

        C C′ CongruenceABBA

        ((B ≠ C) ∧
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))))
          introduceAntecedent

        composeConjunction

Applying outer five segment gives us D′ C′ ≡ D C. We flip the order of the points to turn that into C′ D′ ≡ C D.

        B C D′ B′ C′ D C′ C OuterFiveSegment
        applySyllogism

        D′ C′ D C CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism
))

We now turn to the B = C case. We first note that in this case C′ B′ ≡ C B implies B′ = C′

thm (bprime-cprime () ()
  (((B = C) ∧
    ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))) →
  (B′ = C′)) (
        (B = C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionRightElimination

        (B = C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C′ B′ C B CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        C B C′ B′ CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        B C B′ C′ CongruenceIdentityFromEquality
        import
        applySyllogism
))

thm (cprime-dprime-c-d-case-bc-1 () ()
  ((((B″ = B′) ∧ (B′ = C′)) ∧ (D′ B″ ≡ D B)) → (C′ D′ ≡ B D)) (
        B″ B′ C′ EqualityTransitivity

        D′ EqualityReflexivity
        D EqualityReflexivity
        B EqualityReflexivity
        D′ D′ B″ C′ D D B B CongruenceBuilder
        detach2of2
        detach2of2
        detach1of2

        eliminateBiconditionalReverseInConsequent

The top thing on the proof stack is now B″ = C′ → (D′ B″ ≡ D B → D′ C′ ≡ D B. We just need to combine it with the other thing on the proof stack, import, and adjust the consequent.

        applySyllogism

        import

        D′ C′ D B CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism
))

thm (cprime-dprime-c-d-case-bc-2 () ()
  (((((B″ = B′) ∧ (B′ = C′)) ∧ (D′ B″ ≡ D B)) ∧ (B = C))
    → (C′ D′ ≡ C D)) (
        (((B″ = B′) ∧ (B′ = C′)) ∧ (D′ B″ ≡ D B)) (B = C)
          ConjunctionRightElimination
        B″ B′ C′ D′ D B cprime-dprime-c-d-case-bc-1
        applySyllogism

        (((B″ = B′) ∧ (B′ = C′)) ∧ (D′ B″ ≡ D B)) (B = C)
          ConjunctionLeftElimination
        C′ EqualityReflexivity
        D′ EqualityReflexivity
        D EqualityReflexivity
        C′ C′ D′ D′ B C D D CongruenceBuilder
        detach2of2
        detach2of3
        detach1of2
        applySyllogism

        eliminateBiconditionalReverseInConsequent

        composeConjunction

        (C′ D′ ≡ B D) (C′ D′ ≡ C D) ModusPonens
        applySyllogism
))

thm (cprime-dprime-c-d-case-bc () ()
  (((B = C) ∧
    ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))) →
  (C′ D′ ≡ C D)) (

We've proved all the interesting parts. We just need to pick out the various antecedents for cprime-dprime-c-d-case-bc-2. B″ = B′:

        (B = C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        A D C′ C D′ B′ B B″ bdoubleprime-bprime
        applySyllogism

B′ = C′

        B C A D C′ D′ B′ B″ bprime-cprime
        composeConjunction

D′ B″ ≡ D B

        (B = C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent
        composeConjunction

B = C:

        (B = C)
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ConjunctionRightElimination
        composeConjunction

        B″ B′ C′ D′ D B C cprime-dprime-c-d-case-bc-2
        applySyllogism
))

Finishing the proof of C′ D′ ≡ C D just involves assembling the two cases.

thm (cprime-dprime-c-d () ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (C′ D′ ≡ C D)) (
        B C A D C′ D′ B′ B″ cprime-dprime-c-d-case-bc
        export

        B C A D C′ D′ B′ B″ cprime-dprime-c-d-case-bnotc
        export

        eliminateCases
))

Construction of E

We're now ready to construct the point E. We already have the betweenness relationships we need for the axiom of Pasch, between D′ C A and between C′ D A. Applying Pasch, we get C E C′ and D E D′.

thm (e-exists-1
  ((e A) (e D) (e C′) (e C) (e D′) (e B′) (e B) (e B″)) ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (∃ e ((between C (value e) C′) ∧ (between D (value e) D′)))) (
        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        A C D′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        (((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B)))
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D C′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        D′ C A C′ D e Pasch
        applySyllogism
))

Here's a variant of the previous theorem with the antecedent repeated inside the quantifier.

thm (e-exists
  ((e A) (e D) (e C′) (e C) (e D′) (e B′) (e B) (e B″)) ()
  (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) →
  (∃ e
    (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
      ((between A C D′) ∧ (C D′ ≡ C D))) ∧
      ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
      ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
      (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
      ((between C (value e) C′) ∧ (between D (value e) D′))))) (
        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ImplicationReflexivity

        A D C′ C D′ B′ B B″ e e-exists-1

        composeConjunction

        e
          ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C (value e) C′) ∧ (between D (value e) D′))
          ThereExistsConjunctionMovement
        eliminateBiconditionalForward

        applySyllogism
))

E C ≡ E C′

E C ≡ E C′ and E D ≡ E D′

Here we apply inner five segment to prove E C ≡ E C′. We are applying inner five segment to the line segments D E D′ and D E D′ and points C and C′.

thm (e-c-e-cprime () ()
  ((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) →
  (E C ≡ E C′)) (

First we need between D E D′, which is one of our antecedents.

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionLeftElimination
        eliminateLeftConjunctInConsequent

Secondly we need a second copy of between D E D′.

        (between D E D′) ConjunctionIdempotence
        eliminateBiconditionalReverse
        applySyllogism

Thirdly we need D D′ ≡ D D′, which is an identity.

        D D′ CongruenceReflexivity
        (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′)))
          introduceAntecedent
        composeConjunction

Fourth we need E D′ ≡ E D′, which is an identity.

        E D′ CongruenceReflexivity
        (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′)))
          introduceAntecedent
        composeConjunction

Next we need D C ≡ D C′, which is one of our antecedents (slightly rearranged).

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

        D C′ C D CongruenceRightCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        D C′ D C CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Finally we need D′ C ≡ D′ C′, which follows from the antecedent C D′ ≡ C D and C′ D′ ≡ C D, which we proved previously.

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        A D C′ C D′ B′ B B″ cprime-dprime-c-d
        applySyllogism

        C′ D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        C D′ C D C′ D′ CongruenceTransitivity
        applySyllogism

        C D′ C′ D′ CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Applying inner five segment we get E C ≡ E C′

        D E D′ D E D′ C C′ InnerFiveSegment
        applySyllogism
))

E D ≡ E D′

The proof that E D ≡ E D′ is exactly analogous, but applies inner five segment to the line segments C E C′ and C E C′ and points D and D′.

thm (e-d-e-dprime () ()
  ((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) →
  (E D ≡ E D′)) (

First we need between C E C′, which is one of our antecedents.

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent

Secondly we need a second copy of between C E C′.

        (between C E C′) ConjunctionIdempotence
        eliminateBiconditionalReverse
        applySyllogism

Thirdly we need C C′ ≡ C C′, which is an identity.

        C C′ CongruenceReflexivity
        (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′)))
          introduceAntecedent
        composeConjunction

Fourth we need E C′ ≡ E C′, which is an identity.

        E C′ CongruenceReflexivity
        (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′)))
          introduceAntecedent
        composeConjunction

Next we need C D ≡ C D′, which is one of our antecedents (slightly rearranged).

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Finally we need C′ D ≡ C′ D′, which follows from the antecedent D C′ ≡ C D and C′ D′ ≡ C D, which we proved previously.

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent

        ((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D)))
          ((between C E C′) ∧ (between D E D′))
          ConjunctionRightElimination
        A D C′ C D′ B′ B B″ cprime-dprime-c-d
        applySyllogism

        C′ D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        D C′ C D C′ D′ CongruenceTransitivity
        applySyllogism

        D C′ C′ D′ CongruenceLeftCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Applying inner five segment we get E D ≡ E D′

        C E C′ C E C′ D D′ InnerFiveSegment
        applySyllogism
))

Construction of P, Q, and R

construction of P, Q, and R

Extend C′ C by the distance C D′ to a point P. Extend D′ C by the distance C E to a point R. Extend P R by the distance R P to a point Q.

In other words, we are adding (between C′ C P ∧ C P ≡ C D′) ∧ (between D′ C R ∧ C R ≡ C E) ∧ (between P R Q ∧ R Q ≡ R P)

thm (p-q-r-exist
  ((p q r A) (p q r D) (p q r C′) (p q r C) (p q r D′) (p q r B′) (p q r B) (p q r B″) (p q r E)) ()
  ((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) →
  (∃ r (∃ p (∃ q (
    (((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))) ∧
    ((between D′ C (value r)) ∧ (C (value r) ≡ C E))) ∧
    ((between (value p) (value r) (value q)) ∧ ((value r) (value q) ≡ (value r) (value p)))
  ))))) (
        (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′)))
          ImplicationReflexivity

We're ready to construct p.

        p C′ C C D′ SegmentConstruction
        introduceRightConjunctToConsequent

        p
          (((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′)))
          ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))
          ThereExistsConjunctionMovement
        eliminateBiconditionalForward
        applySyllogism

The construction of r is similar.

        r D′ C C E SegmentConstruction
        introduceRightConjunctToConsequent

        # TODO: this can be simplified via ThereExistsScattering, right?
        r
          (∃ p 
            ((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′))) ∧
            ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))))
          ((between D′ C (value r)) ∧ (C (value r) ≡ C E))
          ThereExistsConjunctionMovement
        eliminateBiconditionalForward
        applySyllogism

        p
          ((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′))) ∧
            ((between C′ C (value p)) ∧ (C (value p) ≡ C D′)))
          ((between D′ C (value r)) ∧ (C (value r) ≡ C E))
          ThereExistsConjunctionRightMovement
        eliminateBiconditionalForward
        r addThereExists
        applySyllogism

The construction of q is only slightly different (with the most obvious difference in the logic being that it depends on p and r).

        q (value p) (value r) (value r) (value p) SegmentConstruction
        p generalize
        r generalize
        introduceRightConjunctToConsequent

        r
          (∃ p (((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′))) ∧
            ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))) ∧
            ((between D′ C (value r)) ∧ (C (value r) ≡ C E))))
          (∀ p (∃ q ((between (value p) (value r) (value q)) ∧ ((value r) (value q) ≡ (value r) (value p)))))
          ThereExistsConjunctionRightCombining
        applySyllogism

        p
          (((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′))) ∧
            ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))) ∧
            ((between D′ C (value r)) ∧ (C (value r) ≡ C E)))
          (∃ q ((between (value p) (value r) (value q)) ∧ ((value r) (value q) ≡ (value r) (value p))))
          ThereExistsConjunctionRightCombining
        r addThereExists
        applySyllogism

        q
          (((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
            ((between A C D′) ∧ (C D′ ≡ C D))) ∧
            ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
            ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
            (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
            ((between C E C′) ∧ (between D E D′))) ∧
            ((between C′ C (value p)) ∧ (C (value p) ≡ C D′))) ∧
            ((between D′ C (value r)) ∧ (C (value r) ≡ C E)))
          ((between (value p) (value r) (value q)) ∧ ((value r) (value q) ≡ (value r) (value p)))
          ThereExistsConjunctionMovement
        eliminateBiconditionalForward
        p addThereExists
        r addThereExists
        applySyllogism
))

C ≠ D′

Our goal is to prove C = C′ ∨ D = D′. We do this by adding C ≠ C′ to our antecedent and then showing it implies D = D′. The first step is to show that C ≠ D′. This is a straightforward consequence of C ≠ C′ and the congruence of C D′ and C′ D′, but it will take a few lemmas to do all the needed arranging.

thm (dprime-cprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C = D′)) →
  (D′ = C′)) (

First we need C = D′.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C = D′)
          ConjunctionLeftElimination

Secondly we need C D′ ≡ D′ C′ which we derive from C D′ ≡ C D (an antecedent), C′ D′ ≡ C D (previously proved), and a bit of rearrangement.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C = D′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C = D′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D C′ C D′ B′ B B″ cprime-dprime-c-d
        applySyllogism

        C′ D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        C D′ C D C′ D′ CongruenceTransitivity
        applySyllogism

        C D′ C′ D′ CongruenceRightCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Now we can show D′ = C′.

        C D′ D′ C′ CongruenceIdentityFromEquality
        import
        applySyllogism
))

thm (c-cprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C = D′)) →
  (C = C′)) (
        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C = D′)
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ E P R Q dprime-cprime

        composeConjunction

        C D′ C′ EqualityTransitivity
        applySyllogism
))

thm (c-dprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (C ≠ D′)) (
        A D C′ C D′ B′ B B″ E P R Q c-cprime
        export

        (C = D′) (C = C′) Transposition
        eliminateBiconditionalReverse
        applySyllogism

        import
))

R P ≡ E D′

The proof is by outer five segment on D′ C R and P C E and points P and D′. We pretty much have everything we need to apply outer five segment, although between P C E is complicated enough to break out into its own lemma. This lemma follows from between P C C′ and between C E C′.

thm (p-c-e () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (between P C E)) (
        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        C′ C P BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

        P C C′ E BetweennessInnerTransitivity
        applySyllogism
))

thm (r-p-e-dprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (R P ≡ E D′)) (

First we need D′ ≠ C. We proved it in the previous section.

        A D C′ C D′ B′ B B″ E P R Q c-dprime

        C D′ EqualitySymmetry
        addNegation
        eliminateBiconditionalReverse
        applySyllogism

Next is between D′ C R, from the construction of R.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

Next is between P C E.

        A D C′ C D′ B′ B B″ E P R Q p-c-e
        composeConjunction

Next is D′ C ≡ P C, from the construction of P.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C P C D′ CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        P C D′ C CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Next is C R ≡ C E, from the construction of R.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        composeConjunction

Next is D′ P ≡ P D′, which holds trivially.

        D′ P CongruenceABBA
        introduceRightConjunctToConsequent

Next is C P ≡ C D′, from the construction of P.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        composeConjunction

We can then conclude R P ≡ E D′.

        D′ C R P C E P D′ OuterFiveSegment
        applySyllogism
))

R Q ≡ E D

This is an easy consequence of R P ≡ E D′.

thm (r-q-e-d () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (R Q ≡ E D)) (

We start with R Q ≡ R P (from the construction of Q).

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

Next is R P ≡ E D′ (from the previous section).

        A D C′ C D′ B′ B B″ E P R Q r-p-e-dprime
        composeConjunction

        R Q R P E D′ CongruenceTransitivity
        applySyllogism

Finally is E D′ ≡ E D (which we proved a few sections back).

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D C′ C D′ B′ B B″ E e-d-e-dprime
        applySyllogism

        E D E D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        R Q E D′ E D CongruenceTransitivity
        applySyllogism
))

D′ D ≡ P Q

D′ D ≡ P Q and C P ≡ C Q

The congruences from the previous section, R P ≡ E D′ and R Q ≡ E D, lead to D′ D ≡ P Q, which is a congruence we'll need later on. The proof is by outer three segment on D′ E D and P R Q.

thm (dprime-d-p-q () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (D′ D ≡ P Q)) (

First is between D′ E D

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        D E D′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

Next is between P R Q

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

Next is D′ E ≡ P R.

        A D C′ C D′ B′ B B″ E P R Q r-p-e-dprime

        R P E D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        E D′ R P CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Last is E D ≡ R Q.

        A D C′ C D′ B′ B B″ E P R Q r-q-e-d

        R Q E D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        D′ E D P R Q OuterThreeSegment
        applySyllogism
))

C Q ≡ C D

D′ D ≡ P Q and C P ≡ C Q

To prove C Q ≡ C D, there are two cases, based on whether D′ = E or not.

D′ = E case

We start with the case in which D′ = E.

First is D′ = D, which follows via E = D from E D ≡ E D′.

thm (c-q-c-d-case-dprime-e-e-d () ()
  (
    ((D′ = E) ∧
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′))) →
  (E = D)) (
        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionRightElimination

        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D C′ C D′ B′ B B″ E e-d-e-dprime
        applySyllogism

        E D E D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        E D′ E D CongruenceLeftCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        D′ E E D CongruenceIdentityFromEquality
        import

        applySyllogism
))

thm (c-q-c-d-case-dprime-e-dprime-d () ()
  (
    ((D′ = E) ∧
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′))) →
  (D′ = D)) (
        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionRightElimination

        D′ E A D C′ C B′ B B″ P R Q c-q-c-d-case-dprime-e-e-d
        composeConjunction

        D′ E D EqualityTransitivity
        applySyllogism
))

It might seem that having proved D′ = D we are done with this case (since after all, D′ = D is the long-term goal of this proof). Although we could, of course, proceed this way, it would entail carrying along the two cases to almost the end of the proof. So we instead will take a few more steps to prove C Q ≡ C D. The next one is P = Q.

thm (c-q-c-d-case-dprime-e-p-q () ()
  (
    ((D′ = E) ∧
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′))) →
  (P = Q)) (
        D′ E A D C′ C B′ B B″ P R Q c-q-c-d-case-dprime-e-dprime-d

        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        A D C′ C D′ B′ B B″ E P R Q dprime-d-p-q
        applySyllogism

        composeConjunction

        D′ D P Q CongruenceIdentityFromEquality
        import

        applySyllogism
))

Now that we have P = Q, we just need to apply transitivity and a substitution to C P ≡ C D′ and C D′ ≡ C D to get C Q = C D.

thm (c-q-c-d-case-dprime-e () ()
  (
    ((D′ = E) ∧
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′))) →
  (C Q ≡ C D)) (
        D′ E A D C′ C B′ B B″ P R Q c-q-c-d-case-dprime-e-p-q

Now we need C P ≡ C D.

        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        (D′ = E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        composeConjunction

        C P C D′ C D CongruenceTransitivity
        applySyllogism

        composeConjunction

P = Q → (C P ≡ C D ↔ C Q ≡ C D)

        C EqualityReflexivity
        C EqualityReflexivity
        D EqualityReflexivity
        C C P Q C C D D CongruenceBuilder
        detach2of2
        detach2of2
        detach1of2

A bit of rearranging and we are done.

        eliminateBiconditionalReverseInConsequent
        import
        applySyllogism
))

D′ ≠ E case

The more interesting case is D′ ≠ E. It follows from outer five segment on line segments D′ E D and P R Q and points C and C.

thm (c-q-c-d-case-dprime-not-e () ()
  (
    ((D′ ≠ E) ∧
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′))) →
  (C Q ≡ C D)) (

First we need D′ ≠ E.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionRightElimination

Next we need between D′ E D.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        D E D′ BetweennessSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Next is between P R Q.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        composeConjunction

Next is D′ E ≡ P R, which we proved a few sections back.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ E P R Q r-p-e-dprime
        applySyllogism

        R P E D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        E D′ R P CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Next is E D ≡ R Q, which we proved a few sections back.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination

        A D C′ C D′ B′ B B″ E P R Q r-q-e-d
        applySyllogism

        R Q E D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Here is D′ C ≡ P C, from the construction of P.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C P C D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        C D′ C P CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

Finally we need E C ≡ R C, which comes from the construction of R.

        (D′ ≠ E)
          (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P))) ∧
          (C ≠ C′))
          ConjunctionLeftElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C R C E CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        C E C R CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

From outer five segment we can conclude D C ≡ Q C.

        D′ E D P R Q C C OuterFiveSegment
        applySyllogism

        D C Q C CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        Q C D C CongruenceCommutativity
        eliminateBiconditionalReverse
        applySyllogism
))

Combining the two cases

thm (c-q-c-d () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (C Q ≡ C D)) (
        D′ E A D C′ C B′ B B″ P R Q c-q-c-d-case-dprime-e
        export

        D′ E A D C′ C B′ B B″ P R Q c-q-c-d-case-dprime-not-e
        export

        eliminateCases
))

A Corollary: C P ≡ C Q

That the previous result implies C P ≡ C Q is apparent from looking at the single ticked line segments in the diagram. The proof is just some congruence transitivity.

thm (c-p-c-q () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (C P ≡ C Q)) (
        A D C′ C D′ B′ B B″ E P R Q c-q-c-d

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C D′ C D CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        C Q C D C D′ CongruenceTransitivity
        applySyllogism

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        C P C D′ CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism

        composeConjunction

        C Q C D′ C P CongruenceTransitivity
        applySyllogism

        C Q C P CongruenceSymmetry
        eliminateBiconditionalReverse
        applySyllogism
))

The line containing C, R, D′, B, B′, C′, and P

D′ P ≡ D′ Q, B P ≡ B Q, and likewise for B′ and C′

We've set up the dominos, and in this section we push them over. For a domino (point) x to "fall" means that we prove x P ≡ x Q (via EquidistantLine). So we need three collinear points, the first two of which are not equal, and the first two of which already have their congruences with P and Q proven. That gives us the third congruence, and then this domino is ready to push on one of the following ones.

D′

We start with R, C, and D′.

The first part is R ≠ C. We will show that R = C implies C = C′, so a transposition gives us what we want.

thm (c-e-lemma () ()
  (((C R ≡ C E) ∧ (R = C)) → (C = E)) (
        C R C E CongruenceLeftCommutativity
        eliminateBiconditionalReverse

        R C C E CongruenceIdentityFromEquality
        applyComm
        applySyllogism

        import
))

thm (c-e () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (R = C)) →
  (C = E)) (
        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (R = C)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateLeftConjunctInConsequent

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (R = C)
          ConjunctionLeftElimination

        composeConjunction

        C R E c-e-lemma

        applySyllogism
))

thm (e-cprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (R = C)) →
  (E = C′)) (
        A D C′ C D′ B′ B B″ E P R Q c-e

        C E EqualitySymmetry
        eliminateBiconditionalReverse
        applySyllogism

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (R = C)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent
        eliminateRightConjunctInConsequent

        A D C′ C D′ B′ B B″ E e-c-e-cprime
        applySyllogism

        composeConjunction

        E C E C′ CongruenceIdentityFromEquality
        import

        applySyllogism
))

thm (r-c-implies-c-cprime () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (R = C)) →
  (C = C′)) (
        A D C′ C D′ B′ B B″ E P R Q c-e
        A D C′ C D′ B′ B B″ E P R Q e-cprime
        composeConjunction

        C E C′ EqualityTransitivity
        applySyllogism
))

thm (r-not-c () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (R ≠ C)) (
        A D C′ C D′ B′ B B″ E P R Q r-c-implies-c-cprime
        export

        (R = C) (C = C′) Transposition
        eliminateBiconditionalReverse
        applySyllogism

        import
))

Now we are ready to prove D′ P ≡ D′ Q.

thm (dprime-p-dprime-q () ()
  (
    (((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
    ((between A C D′) ∧ (C D′ ≡ C D))) ∧
    ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
    ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
    (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
    ((between C E C′) ∧ (between D E D′))) ∧
    ((between C′ C P) ∧ (C P ≡ C D′))) ∧
    ((between D′ C R) ∧ (C R ≡ C E))) ∧
    ((between P R Q) ∧ (R Q ≡ R P))) ∧
    (C ≠ C′)) →
  (D′ P ≡ D′ Q)) (

First we need R ≠ C.

        A D C′ C D′ B′ B B″ E P R Q r-not-c

Next is collinear R C D′.

        ((((((((((between A D C′) ∧ (D C′ ≡ C D)) ∧
          ((between A C D′) ∧ (C D′ ≡ C D))) ∧
          ((between A C′ B′) ∧ (C′ B′ ≡ C B))) ∧
          ((between A D′ B″) ∧ (D′ B″ ≡ D B))) ∧
          (((A ≠ B) ∧ (between A B C)) ∧ (between A B D))) ∧
          ((between C E C′) ∧ (between D E D′))) ∧
          ((between C′ C P) ∧ (C P ≡ C D′))) ∧
          ((between D′ C R) ∧ (C R ≡ C E))) ∧
          ((between P R Q) ∧ (R Q ≡ R P)))
          (C ≠ C′)
          ConjunctionRightElimination
        eliminateRightConjunctInConsequent
        eliminateLeftConjunctInConsequent
        eliminateRightConjunctInConsequent

        D′ C R