Metamath Proof Explorer

Theorem btwnconn1lem8

Description: Lemma for btwnconn1 . Now, we introduce the last three points used in the construction: P , Q , and R will turn out to be equal further down, and will provide us with the key to the final statement. We begin by establishing congruence of R P and E d . (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem8 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )

Proof

Step Hyp Ref Expression
1 simpr2l ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ )
2 1 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ )
3 simpr1r ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ )
4 3 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ )
5 simp11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
6 simp2l1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simp31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simp2r1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
9 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ) )
10 5 6 7 6 8 9 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ) )
11 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
12 5 7 6 8 6 11 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
13 10 12 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
14 13 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
15 4 14 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ )
16 simp33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simp2r3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simp2l3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
19 simpr1l ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ )
20 19 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ )
21 5 6 18 7 20 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐶 Btwn ⟨ 𝑃 , 𝑐 ⟩ )
22 simprll ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ )
23 22 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ )
24 btwnintr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝑃 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ) → 𝐶 Btwn ⟨ 𝑃 , 𝐸 ⟩ ) )
25 5 7 6 17 18 24 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝑃 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ) → 𝐶 Btwn ⟨ 𝑃 , 𝐸 ⟩ ) )
26 25 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝑃 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ) → 𝐶 Btwn ⟨ 𝑃 , 𝐸 ⟩ ) )
27 21 23 26 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐶 Btwn ⟨ 𝑃 , 𝐸 ⟩ )
28 simpr2r ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ )
29 28 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ )
30 5 8 6 16 7 6 17 2 27 15 29 cgrextendand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝑅 ⟩ Cgr ⟨ 𝑃 , 𝐸 ⟩ )
31 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝑑 , 𝑅 ⟩ Cgr ⟨ 𝑃 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ) )
32 5 8 6 16 7 6 17 31 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝑑 , 𝑅 ⟩ Cgr ⟨ 𝑃 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ) )
33 32 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝑑 , 𝑅 ⟩ Cgr ⟨ 𝑃 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ) )
34 15 30 29 33 mpbir3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ )
35 5 8 7 cgrrflx2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ )
36 35 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ )
37 36 4 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) )
38 2 34 37 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) )
39 simp1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
40 simp2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) )
41 simp2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) )
42 39 40 41 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
43 simpl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) )
44 simprl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) )
45 43 44 jca ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) )
46 btwnconn1lem7 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → 𝐶 ≠ 𝑑 )
47 42 45 46 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐶 ≠ 𝑑 )
48 47 necomd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝑑 ≠ 𝐶 )
49 brofs2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑑 , 𝐶 ⟩ , ⟨ 𝑅 , 𝑃 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝐶 ⟩ , ⟨ 𝐸 , 𝑑 ⟩ ⟩ ↔ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) ) )
50 49 anbi1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑑 , 𝐶 ⟩ , ⟨ 𝑅 , 𝑃 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝐶 ⟩ , ⟨ 𝐸 , 𝑑 ⟩ ⟩ ∧ 𝑑 ≠ 𝐶 ) ↔ ( ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) ∧ 𝑑 ≠ 𝐶 ) ) )
51 5segofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑑 , 𝐶 ⟩ , ⟨ 𝑅 , 𝑃 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝐶 ⟩ , ⟨ 𝐸 , 𝑑 ⟩ ⟩ ∧ 𝑑 ≠ 𝐶 ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ) )
52 50 51 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) ∧ 𝑑 ≠ 𝐶 ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ) )
53 5 8 6 16 7 7 6 17 8 52 syl333anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) ∧ 𝑑 ≠ 𝐶 ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ) )
54 53 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ( ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐶 , 𝑅 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝐶 , 𝐸 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) ∧ 𝑑 ≠ 𝐶 ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ) )
55 38 48 54 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )