Theorem btwnconn1lem9

Description: Lemma for btwnconn1 . Now, a quick use of transitivity to establish congruence on R Q and E D . (Contributed by Scott Fenton, 8-Oct-2013)

	Ref	Expression
Assertion	btwnconn1lem9	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 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		simp11	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2		simp33	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
3		simp32	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
4		simp2r3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simp2l2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6		simp2r1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
7		simp31	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
8		simpr3r	⊢ ( ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ )
9	8	ad2antll	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ )
10		btwnconn1lem8	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑃 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )
11	1 2 3 2 7 4 6 9 10	cgrtrand	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )
12		simp1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
13		simp2l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) )
14		simp2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) )
15	12 13 14	3jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
16		simpl	⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) )
17		simprl	⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) )
18	16 17	jca	⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) → ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) )
19		btwnconn1lem6	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ) ) → ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )
20	15 18 19	syl2an	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝐸 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑑 ⟩ )
21	1 2 3 4 5 4 6 11 20	cgrtr3and	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ∧ ( ( 𝐸 Btwn ⟨ 𝐶 , 𝑐 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝑑 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝑐 , 𝑃 ⟩ ∧ ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑑 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝑑 , 𝑅 ⟩ ∧ ⟨ 𝐶 , 𝑅 ⟩ Cgr ⟨ 𝐶 , 𝐸 ⟩ ) ∧ ( 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ∧ ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝑅 , 𝑃 ⟩ ) ) ) ) ) → ⟨ 𝑅 , 𝑄 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ )