Metamath Proof Explorer

Theorem btwnconn1lem13

Description: Lemma for btwnconn1 . Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem13 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐶 = 𝑐 ∨ 𝐷 = 𝑑 ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝐶 ≠ 𝑐 ↔ ¬ 𝐶 = 𝑐 )
2 simp2rl ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ )
3 2 adantr ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ )
4 simp2ll ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
5 4 adantr ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
6 3 5 jca ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ) )
7 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
8 simprl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simprrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
11 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ↔ 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ) )
12 7 8 9 10 11 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ↔ 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ) )
13 simprl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simprl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
15 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ↔ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) )
16 7 13 9 14 15 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ↔ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) )
17 12 16 anbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ∧ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) ) )
18 6 17 imbitrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ( 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ∧ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) ) )
19 axpasch ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ∧ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) )
20 7 10 14 9 8 13 19 syl132anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝑑 , 𝐴 ⟩ ∧ 𝐷 Btwn ⟨ 𝑐 , 𝐴 ⟩ ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) )
21 18 20 syld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) )
22 21 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) )
23 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
24 14 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
25 8 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
26 10 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
27 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) )
28 23 24 25 25 26 27 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) )
29 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
30 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) )
31 23 26 25 25 29 30 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) )
32 reeanv ⊢ ( ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ↔ ( ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) )
33 28 31 32 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) )
34 33 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) )
35 7 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
36 simprl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) )
37 simprr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) )
38 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) )
39 35 36 37 37 36 38 syl122anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) )
40 39 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) )
41 simp-4l ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
42 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) )
43 42 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) )
44 10 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
45 simprrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
46 45 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
47 simpllr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
48 44 46 47 3jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) )
49 43 48 jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
50 simplrl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) )
51 simpr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) )
52 simplrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) )
53 50 51 52 3jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) )
54 41 49 53 3jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
55 simp1ll ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐴 ≠ 𝐵 )
56 55 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) → 𝐴 ≠ 𝐵 )
57 56 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → 𝐴 ≠ 𝐵 )
58 simp1lr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐵 ≠ 𝐶 )
59 58 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) → 𝐵 ≠ 𝐶 )
60 59 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → 𝐵 ≠ 𝐶 )
61 simpllr ⊢ ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) → 𝐶 ≠ 𝑐 )
62 61 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → 𝐶 ≠ 𝑐 )
63 57 60 62 3jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) )
64 simpl1r ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
65 64 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
66 63 65 jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
67 simpll2 ⊢ ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
68 67 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
69 simpl3l ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) )
71 simpl3r ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) → ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) )
72 71 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) )
73 70 72 jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) )
74 66 68 73 3jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 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 ⟨ 𝐷 , 𝐵 ⟩ ) ) ) )
75 simpllr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) )
76 simplrl ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) )
77 simplrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) )
78 simpr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) )
79 76 77 78 3jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) → ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) )
80 74 75 79 jca32 ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 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 ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) ) ) )
81 btwnconn1lem12 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) ) ) ) → 𝐷 = 𝑑 )
82 54 80 81 syl2an ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) ) → 𝐷 = 𝑑 )
83 82 an4s ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ) ∧ ( 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ∧ ⟨ 𝑟 , 𝑞 ⟩ Cgr ⟨ 𝑟 , 𝑝 ⟩ ) ) ) → 𝐷 = 𝑑 )
84 40 83 rexlimddv ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ) → 𝐷 = 𝑑 )
85 84 an4s ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) ) ) → 𝐷 = 𝑑 )
86 85 exp32 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) → 𝐷 = 𝑑 ) ) )
87 86 rexlimdvv ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → ( ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑝 ⟩ ∧ ⟨ 𝐶 , 𝑝 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑟 ⟩ ∧ ⟨ 𝐶 , 𝑟 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ) → 𝐷 = 𝑑 ) )
88 34 87 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → 𝐷 = 𝑑 )
89 88 an4s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑒 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝑒 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → 𝐷 = 𝑑 )
90 22 89 rexlimddv ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ 𝐶 ≠ 𝑐 ) ) → 𝐷 = 𝑑 )
91 90 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐶 ≠ 𝑐 → 𝐷 = 𝑑 ) )
92 1 91 biimtrrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( ¬ 𝐶 = 𝑐 → 𝐷 = 𝑑 ) )
93 92 orrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐶 = 𝑐 ∨ 𝐷 = 𝑑 ) )