Theorem outsideofeu

Description: Given a nondegenerate ray, there is a unique point congruent to the segment B C lying on the ray A R . Theorem 6.11 of Schwabhauser p. 44. (Contributed by Scott Fenton, 23-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	outsideofeu	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → ∃! 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		segcon2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
2	1	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
3		simpl1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
4		simpl2l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
6		simpl2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
7		broutsideof2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
8	3 4 5 6 7	syl13anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
9	8	adantr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
10		simp3	⊢ ( ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) → ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
11		simpllr	⊢ ( ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) → 𝐵 ≠ 𝐶 )
12	11	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → 𝐵 ≠ 𝐶 )
13		simprlr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
14		simp2l	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
15	14	anim1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) )
16		simpl3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
17		cgrdegen	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 = 𝑥 ↔ 𝐵 = 𝐶 ) ) )
18	3 15 16 17	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 = 𝑥 ↔ 𝐵 = 𝐶 ) ) )
19	18	adantr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 = 𝑥 ↔ 𝐵 = 𝐶 ) ) )
20	13 19	mpd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ( 𝐴 = 𝑥 ↔ 𝐵 = 𝐶 ) )
21	20	necon3bid	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ( 𝐴 ≠ 𝑥 ↔ 𝐵 ≠ 𝐶 ) )
22	12 21	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → 𝐴 ≠ 𝑥 )
23	22	necomd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → 𝑥 ≠ 𝐴 )
24		simplll	⊢ ( ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) → 𝑅 ≠ 𝐴 )
25	24	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → 𝑅 ≠ 𝐴 )
26		simprr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
27	23 25 26	3jca	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) → ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) )
28	27	expr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) → ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
29	10 28	impbid2	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ( 𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) ↔ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) )
30	9 29	bitrd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ) )
31		orcom	⊢ ( ( 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ∨ 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) ↔ ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) )
32	30 31	bitrdi	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ) )
33	32	expr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ) ) )
34	33	pm5.32rd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
35	34	an32s	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
36	35	rexbidva	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑅 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝑅 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
37	2 36	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
38		simpl1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
39		simpl2l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
40		simpl2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
41		simpl3l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
42	39 40 41	3jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
43		simpl3r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
44		simprl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
45		simprr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
46	43 44 45	3jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) )
47	38 42 46	3jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
48		simpr	⊢ ( ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
49		outsideofeq	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑥 = 𝑦 ) )
50	49	imp	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑥 = 𝑦 )
51	47 48 50	syl2an	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ) → 𝑥 = 𝑦 )
52	51	an4s	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ) → 𝑥 = 𝑦 )
53	52	exp32	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑥 = 𝑦 ) ) )
54	53	ralrimivv	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ∀ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑥 = 𝑦 ) )
55		opeq1	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑅 ⟩ = ⟨ 𝑦 , 𝑅 ⟩ )
56	55	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ↔ 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ) )
57		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
58	57	breq1d	⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
59	56 58	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
60	59	reu4	⊢ ( ∃! 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ∀ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( ( ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 OutsideOf ⟨ 𝑦 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑦 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑥 = 𝑦 ) ) )
61	37 54 60	sylanbrc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → ∃! 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
62	61	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → ∃! 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 OutsideOf ⟨ 𝑥 , 𝑅 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )