Metamath Proof Explorer

Theorem btwnconn1lem11

Description: Lemma for btwnconn1 . Now, we establish that D and Q are equidistant from C . (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem11 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ )

Proof

Step Hyp Ref Expression
1 btwnconn1lem8 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )
2 btwnconn1lem9 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ )
3 btwnconn1lem10 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ )
4 1 2 3 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) )
5 4 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 = 𝐸 ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) )
6 simpr3r ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ )
7 6 adantl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ )
8 simpr2r ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ )
9 8 adantl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ )
10 7 9 jca ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) )
11 opeq2 ⊢ ( 𝑑 = 𝐸 → ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐸 ⟩ )
12 11 breq2d ⊢ ( 𝑑 = 𝐸 → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) )
13 12 anbi2d ⊢ ( 𝑑 = 𝐸 → ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ↔ ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ) )
14 opeq1 ⊢ ( 𝑑 = 𝐸 → ⟨ 𝑑 , 𝑑 ⟩ = ⟨ 𝐸 , 𝑑 ⟩ )
15 14 breq2d ⊢ ( 𝑑 = 𝐸 → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ↔ ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ) )
16 opeq1 ⊢ ( 𝑑 = 𝐸 → ⟨ 𝑑 , 𝐷 ⟩ = ⟨ 𝐸 , 𝐷 ⟩ )
17 16 breq2d ⊢ ( 𝑑 = 𝐸 → ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ↔ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ) )
18 15 17 3anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ↔ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) )
19 13 18 anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ↔ ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
20 19 biimpar ⊢ ( ( 𝑑 = 𝐸 ∧ ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ) → ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) )
21 simpr1 ⊢ ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ )
22 simp11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
23 simp33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
24 simp31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
25 simp2r1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
26 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ → 𝑅 = 𝑃 ) )
27 22 23 24 25 26 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ → 𝑅 = 𝑃 ) )
28 21 27 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → 𝑅 = 𝑃 ) )
29 opeq1 ⊢ ( 𝑅 = 𝑃 → ⟨ 𝑅 , 𝑄 ⟩ = ⟨ 𝑃 , 𝑄 ⟩ )
30 opeq1 ⊢ ( 𝑅 = 𝑃 → ⟨ 𝑅 , 𝑃 ⟩ = ⟨ 𝑃 , 𝑃 ⟩ )
31 29 30 breq12d ⊢ ( 𝑅 = 𝑃 → ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ↔ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) )
32 opeq2 ⊢ ( 𝑅 = 𝑃 → ⟨ 𝐶 , 𝑅 ⟩ = ⟨ 𝐶 , 𝑃 ⟩ )
33 32 breq1d ⊢ ( 𝑅 = 𝑃 → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) )
34 31 33 anbi12d ⊢ ( 𝑅 = 𝑃 → ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ↔ ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) )
35 30 breq1d ⊢ ( 𝑅 = 𝑃 → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ) )
36 29 breq1d ⊢ ( 𝑅 = 𝑃 → ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ↔ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ) )
37 35 36 3anbi12d ⊢ ( 𝑅 = 𝑃 → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ↔ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) )
38 34 37 anbi12d ⊢ ( 𝑅 = 𝑃 → ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ↔ ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
39 38 biimpac ⊢ ( ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ∧ 𝑅 = 𝑃 ) → ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) )
40 simpll ⊢ ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ )
41 simp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
42 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ → 𝑃 = 𝑄 ) )
43 22 24 41 24 42 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ → 𝑃 = 𝑄 ) )
44 40 43 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → 𝑃 = 𝑄 ) )
45 simprlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ )
46 simpr3 ⊢ ( ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) → ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ )
47 simp2l2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
48 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ → 𝑑 = 𝐷 ) )
49 22 25 47 24 48 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ → 𝑑 = 𝐷 ) )
50 46 49 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) → 𝑑 = 𝐷 ) )
51 50 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → 𝑑 = 𝐷 )
52 51 opeq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
53 52 breq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
54 simp2l1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
55 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ ) )
56 22 54 24 54 47 55 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ ) )
57 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
58 22 24 54 47 54 57 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
59 56 58 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
60 59 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
61 53 60 bitrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
62 45 61 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ )
63 62 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
64 opeq2 ⊢ ( 𝑃 = 𝑄 → ⟨ 𝑃 , 𝑃 ⟩ = ⟨ 𝑃 , 𝑄 ⟩ )
65 64 breq1d ⊢ ( 𝑃 = 𝑄 → ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ↔ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) )
66 65 anbi1d ⊢ ( 𝑃 = 𝑄 → ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ↔ ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ) )
67 64 breq1d ⊢ ( 𝑃 = 𝑄 → ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ↔ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ) )
68 64 breq2d ⊢ ( 𝑃 = 𝑄 → ( ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ↔ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) )
69 67 68 3anbi23d ⊢ ( 𝑃 = 𝑄 → ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ↔ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) )
70 66 69 anbi12d ⊢ ( 𝑃 = 𝑄 → ( ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) ↔ ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
71 opeq1 ⊢ ( 𝑃 = 𝑄 → ⟨ 𝑃 , 𝐶 ⟩ = ⟨ 𝑄 , 𝐶 ⟩ )
72 71 breq2d ⊢ ( 𝑃 = 𝑄 → ( ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ↔ ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
73 70 72 imbi12d ⊢ ( 𝑃 = 𝑄 → ( ( ( ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) ↔ ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) )
74 63 73 syl5ibcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 = 𝑄 → ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) )
75 74 com23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ( 𝑃 = 𝑄 → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) )
76 44 75 mpdd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑃 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑃 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑃 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
77 39 76 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ∧ 𝑅 = 𝑃 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
78 77 expd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ( 𝑅 = 𝑃 → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) )
79 28 78 mpdd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝑑 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
80 20 79 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑑 = 𝐸 ∧ ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
81 80 exp4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑑 = 𝐸 → ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) ) )
82 81 com23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) → ( 𝑑 = 𝐸 → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) ) )
83 10 82 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( 𝑑 = 𝐸 → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) ) ) )
84 83 imp31 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 = 𝐸 ) → ( ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
85 5 84 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 = 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ )
86 simp2r3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
87 simprlr ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ )
88 87 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ )
89 22 86 47 25 88 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ )
90 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝑅 ⟩ Cgr ⟨ 𝑑 , 𝐸 ⟩ ) )
91 22 23 24 86 25 90 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝑅 ⟩ Cgr ⟨ 𝑑 , 𝐸 ⟩ ) )
92 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝑅 ⟩ Cgr ⟨ 𝑑 , 𝐸 ⟩ ↔ ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ) )
93 22 24 23 25 86 92 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝑅 ⟩ Cgr ⟨ 𝑑 , 𝐸 ⟩ ↔ ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ) )
94 91 93 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ) )
95 94 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ) )
96 1 95 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ )
97 22 23 41 86 47 2 cgrcomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝑅 , 𝑄 ⟩ )
98 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝑅 , 𝑄 ⟩ ) ) )
99 22 25 86 47 24 23 41 98 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝑅 , 𝑄 ⟩ ) ) )
100 99 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ↔ ( ⟨ 𝑑 , 𝐸 ⟩ Cgr ⟨ 𝑃 , 𝑅 ⟩ ∧ ⟨ 𝑑 , 𝐷 ⟩ Cgr ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝑅 , 𝑄 ⟩ ) ) )
101 96 3 97 100 mpbir3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ )
102 simpr1r ⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ )
103 102 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ )
104 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ) )
105 22 54 24 54 25 104 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ) )
106 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
107 22 24 54 25 54 106 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝐶 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
108 105 107 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
109 108 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ) )
110 103 109 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ )
111 8 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ )
112 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ↔ ⟨ 𝑅 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐶 ⟩ ) )
113 22 54 23 54 86 112 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ↔ ⟨ 𝑅 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐶 ⟩ ) )
114 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐶 ⟩ ↔ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) )
115 22 23 54 86 54 114 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑅 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐶 ⟩ ↔ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) )
116 113 115 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ↔ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) )
117 116 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ↔ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) )
118 111 117 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ )
119 110 118 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) )
120 89 101 119 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) )
121 120 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 ≠ 𝐸 ) → ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) )
122 simpr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 ≠ 𝐸 ) → 𝑑 ≠ 𝐸 )
123 brofs2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑑 , 𝐸 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝑅 ⟩ , ⟨ 𝑄 , 𝐶 ⟩ ⟩ ↔ ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) ) )
124 123 anbi1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑑 , 𝐸 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝑅 ⟩ , ⟨ 𝑄 , 𝐶 ⟩ ⟩ ∧ 𝑑 ≠ 𝐸 ) ↔ ( ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) ∧ 𝑑 ≠ 𝐸 ) ) )
125 5segofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑑 , 𝐸 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑃 , 𝑅 ⟩ , ⟨ 𝑄 , 𝐶 ⟩ ⟩ ∧ 𝑑 ≠ 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
126 124 125 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) ∧ 𝑑 ≠ 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
127 22 25 86 47 54 24 23 41 54 126 syl333anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) ∧ 𝑑 ≠ 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
128 127 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 ≠ 𝐸 ) → ( ( ( 𝐸 Btwn ⟨ 𝑑 , 𝐷 ⟩ ∧ ⟨ 𝑑 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝑃 , ⟨ 𝑅 , 𝑄 ⟩ ⟩ ∧ ( ⟨ 𝑑 , 𝐶 ⟩ Cgr ⟨ 𝑃 , 𝐶 ⟩ ∧ ⟨ 𝐸 , 𝐶 ⟩ Cgr ⟨ 𝑅 , 𝐶 ⟩ ) ) ∧ 𝑑 ≠ 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ ) )
129 121 122 128 mp2and ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) ∧ 𝑑 ≠ 𝐸 ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ )
130 85 129 pm2.61dane ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐷 , 𝐶 ⟩ Cgr ⟨ 𝑄 , 𝐶 ⟩ )