Metamath Proof Explorer

Theorem cgrxfr

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion cgrxfr ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → 𝑁 ∈ ℕ )
2 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
4 btwndiff ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) )
5 1 2 3 4 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → ∃ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) )
6 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
7 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
11 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
12 6 7 8 9 10 11 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
13 12 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
14 anass ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
15 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
16 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
19 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
20 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
21 15 16 17 18 19 20 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
22 21 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
23 anass ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
24 df-3an ⊢ ( ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) )
25 24 anbi2i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
26 23 25 bitr4i ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
27 simplrr ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐷 ≠ 𝑔 )
28 27 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐷 ≠ 𝑔 )
29 28 necomd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑔 ≠ 𝐷 )
30 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
31 simpr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) )
32 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
33 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
34 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) )
35 simprl ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ )
36 35 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ )
37 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ )
38 30 31 32 33 34 36 37 btwnexchand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ )
39 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
40 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
41 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
42 30 31 32 33 34 36 37 btwnexch3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑒 Btwn ⟨ 𝐷 , 𝑓 ⟩ )
43 simplll ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
44 43 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
45 simprr ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
46 45 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
47 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
48 30 32 33 34 39 40 41 42 44 46 47 cgrextendand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
49 38 48 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) )
50 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
51 simplrl ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ )
52 51 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ )
53 30 32 50 31 52 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ )
54 simpllr ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )
55 54 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )
56 30 39 41 32 50 55 cgrcomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
57 53 56 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) )
58 29 49 57 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑔 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ) )
59 58 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝑔 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ) ) )
60 segconeq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑔 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝑓 = 𝐹 ) )
61 30 32 39 41 31 34 50 60 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑔 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝐷 , 𝑓 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝑓 = 𝐹 ) )
62 59 61 syld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑓 = 𝐹 ) )
63 62 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑓 = 𝐹 )
64 opeq2 ⊢ ( 𝑓 = 𝐹 → ⟨ 𝑔 , 𝑓 ⟩ = ⟨ 𝑔 , 𝐹 ⟩ )
65 64 breq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ↔ 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ) )
66 opeq2 ⊢ ( 𝑓 = 𝐹 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝑒 , 𝐹 ⟩ )
67 66 breq1d ⊢ ( 𝑓 = 𝐹 → ( ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
68 65 67 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
69 68 biimpa ⊢ ( ( 𝑓 = 𝐹 ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
70 simpl ⊢ ( ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ )
71 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ) → 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) )
72 30 31 32 33 50 71 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ) → 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) )
73 35 70 72 syl2ani ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) )
74 73 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ )
75 simplrr ⊢ ( ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
76 75 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
77 30 32 33 39 40 76 cgrcomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ )
78 54 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )
79 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
80 30 33 50 40 41 79 cgrcomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝐹 ⟩ )
81 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝐹 ⟩ ) ) )
82 30 39 40 41 32 33 50 81 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝐹 ⟩ ) ) )
83 82 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝐹 ⟩ ) ) )
84 77 78 80 83 mpbir3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ )
85 74 84 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) )
86 85 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝐹 ⟩ ∧ ⟨ 𝑒 , 𝐹 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
87 69 86 syl5 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝑓 = 𝐹 ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
88 87 expcomd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑓 = 𝐹 → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) ) )
89 88 impr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑓 = 𝐹 → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
90 63 89 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) )
91 90 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
92 26 91 sylanb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
93 92 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
94 93 rexlimdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝑔 , 𝑓 ⟩ ∧ ⟨ 𝑒 , 𝑓 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
95 22 94 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ∧ ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) )
96 95 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
97 14 96 sylanb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
98 97 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
99 98 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) → ( ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝑔 , 𝑒 ⟩ ∧ ⟨ 𝐷 , 𝑒 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
100 13 99 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) )
101 100 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → ( ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
102 101 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) ∧ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
103 102 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → ( ∃ 𝑔 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐹 , 𝑔 ⟩ ∧ 𝐷 ≠ 𝑔 ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )
104 5 103 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) )
105 104 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑒 Btwn ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝑒 , 𝐹 ⟩ ⟩ ) ) )