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 syl5ib ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ( ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐵 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 syl5bir ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( ¬ 𝐶 = 𝑐𝐷 = 𝑑 ) )
93 92 orrd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( ( ( 𝐴𝐵𝐵𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐶 = 𝑐𝐷 = 𝑑 ) )