Metamath Proof Explorer

Theorem outsideofeq

Description: Uniqueness law for OutsideOf . Analogue of segconeq . (Contributed by Scott Fenton, 24-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofeq ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
5 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ↔ ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ) )
6 1 2 3 4 5 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ↔ ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ) )
7 6 anbi1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
8 simp33 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) )
9 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ↔ ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ) )
10 1 2 8 4 9 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ↔ ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ) )
11 10 anbi1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
12 7 11 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ↔ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) )
13 simpll3 ⊢ ( ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) )
14 simprl3 ⊢ ( ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) )
15 13 14 jca ⊢ ( ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) )
16 15 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) )
17 simpll2 ⊢ ( ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑅 ≠ 𝐴 )
18 17 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑅 ≠ 𝐴 )
19 simp23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
20 simp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
21 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
22 simprrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
23 1 2 3 2 8 19 20 21 22 cgrtr3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
24 16 18 23 jca32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) )
25 simprll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ )
26 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ )
27 simprrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
28 midofsegid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) )
29 1 2 4 3 8 28 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) )
30 29 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) )
31 25 26 27 30 mp3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 = 𝑌 )
32 31 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) → ( ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) ) )
33 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ )
34 simprll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ )
35 1 2 8 4 3 33 34 btwnexchand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ )
36 simprrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
37 1 2 3 8 35 36 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 = 𝑌 )
38 37 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) → ( ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) ) )
39 simprll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ )
40 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ )
41 1 2 3 4 8 39 40 btwnexchand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ )
42 simprrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
43 1 2 3 2 8 42 cgrcomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ )
44 1 2 8 3 41 43 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑌 = 𝑋 )
45 44 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 = 𝑌 )
46 45 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ( ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) ) )
47 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ )
48 simplrr ⊢ ( ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
49 48 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
50 1 2 3 2 8 49 cgrcomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ )
51 1 2 8 3 47 50 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → 𝑌 = 𝑋 )
52 51 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → 𝑋 = 𝑌 )
53 52 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ → 𝑋 = 𝑌 ) )
54 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) → 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ )
55 simplrr ⊢ ( ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
56 55 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
57 1 2 3 8 54 56 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) → 𝑋 = 𝑌 )
58 57 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ( 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
59 simprrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑅 ≠ 𝐴 )
60 59 necomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝐴 ≠ 𝑅 )
61 simprll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ )
62 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ )
63 btwnconn1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑅 ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ∨ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) )
64 1 2 4 3 8 63 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑅 ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ∨ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) )
65 64 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ( ( 𝐴 ≠ 𝑅 ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ∨ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) )
66 60 61 62 65 mp3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → ( 𝑋 Btwn ⟨ 𝐴 , 𝑌 ⟩ ∨ 𝑌 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) )
67 53 58 66 mpjaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 = 𝑌 )
68 67 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ∧ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) → ( ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) ) )
69 32 38 46 68 ccased ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) → ( ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) → 𝑋 = 𝑌 ) ) )
70 69 imp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) ) ) → 𝑋 = 𝑌 )
71 24 70 syldan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑋 = 𝑌 )
72 71 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝑋 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑋 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑋 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ( 𝑌 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑌 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑌 ⟩ ) ) ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑋 = 𝑌 ) )
73 12 72 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 OutsideOf ⟨ 𝑋 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑌 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑋 = 𝑌 ) )