Metamath Proof Explorer

Theorem brsegle2

Description: Alternate characterization of segment comparison. Theorem 5.5 of Schwabhauser p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion brsegle2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
2 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
3 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
4 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
7 btwncolinear2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ) )
8 3 4 5 6 7 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ) )
9 8 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ) )
10 2 9 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ )
11 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simprr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
14 3 11 12 4 6 13 cgrcomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
15 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
16 lineext ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) )
17 3 4 6 5 15 16 syl131anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) )
18 17 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ( 𝐶 Colinear ⟨ 𝑦 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) )
19 10 14 18 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ )
20 an32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) )
21 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
22 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
23 22 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
24 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
25 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
26 25 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
27 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
28 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
29 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
30 29 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
31 simplr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
32 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) )
33 21 23 24 26 28 30 31 32 syl133anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) )
34 33 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) )
35 simp2l ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
36 simp3 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) )
37 33 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) )
38 36 37 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ )
39 btwnxfr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
40 21 23 24 26 28 30 31 39 syl133anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
41 40 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
42 35 38 41 mp2and ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ )
43 simp32 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ )
44 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ↔ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
45 21 23 26 28 31 44 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ↔ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
46 45 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ↔ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
47 43 46 mpbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
48 42 47 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
49 48 3expia ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝐵 , 𝑥 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
50 34 49 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
51 20 50 sylanb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
52 51 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
53 52 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
54 19 53 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
55 54 rexlimdva2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
56 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ )
57 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝑁 ∈ ℕ )
58 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
59 simplr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
60 29 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
61 btwncolinear1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ → 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ ) )
62 57 58 59 60 61 syl13anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ → 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ ) )
63 56 62 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ )
64 simprr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
65 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
66 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
67 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
68 lineext ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ) )
69 65 27 66 29 67 68 syl131anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ) )
70 69 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( 𝐴 Colinear ⟨ 𝑥 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ) )
71 63 64 70 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ )
72 27 66 29 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
73 72 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
74 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) )
75 21 73 23 26 24 74 syl113anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) )
76 75 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) )
77 simp2l ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ )
78 simp32 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
79 simp2r ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
80 simp33 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ )
81 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) )
82 21 31 30 26 24 81 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) )
83 82 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ( ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) )
84 80 83 mpbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ )
85 78 79 84 3jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) )
86 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) ) )
87 21 28 30 31 23 24 26 86 syl133anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) ) )
88 87 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝑦 , 𝐷 ⟩ ) ) )
89 85 88 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ )
90 btwnxfr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
91 21 28 30 31 23 24 26 90 syl133anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
92 91 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝑥 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
93 77 89 92 mp2and ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
94 93 78 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
95 94 3expia ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑦 ⟩ ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
96 76 95 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
97 96 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
98 97 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ⟨ 𝐴 , ⟨ 𝑥 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐶 , ⟨ 𝐷 , 𝑦 ⟩ ⟩ → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
99 71 98 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
100 99 rexlimdva2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
101 55 100 impbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
102 1 101 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )