Metamath Proof Explorer

Theorem ifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H G , with B between A and C and F between E and G . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Scott Fenton, 27-Sep-2013)

Ref Expression
Assertion ifscgr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ InnerFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )

Proof

Step Hyp Ref Expression
1 brifs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ InnerFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
2 simp1l ⊢ ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ )
3 simp11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
4 simp13 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simp21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
6 axbtwnid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ → 𝐵 = 𝐶 ) )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ → 𝐵 = 𝐶 ) )
8 2 7 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝐵 = 𝐶 ) )
9 simp2r ⊢ ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ )
10 simp3r ⊢ ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ )
11 9 10 jca ⊢ ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
12 opeq2 ⊢ ( 𝐵 = 𝐶 → ⟨ 𝐵 , 𝐵 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
13 12 breq1d ⊢ ( 𝐵 = 𝐶 → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) )
14 opeq1 ⊢ ( 𝐵 = 𝐶 → ⟨ 𝐵 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
15 14 breq1d ⊢ ( 𝐵 = 𝐶 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
16 13 15 anbi12d ⊢ ( 𝐵 = 𝐶 → ( ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) )
17 16 biimprd ⊢ ( 𝐵 = 𝐶 → ( ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) )
18 11 17 mpan9 ⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐵 = 𝐶 ) → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
19 simp31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
20 simp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
21 cgrid2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ → 𝐹 = 𝐺 ) )
22 3 4 19 20 21 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ → 𝐹 = 𝐺 ) )
23 opeq1 ⊢ ( 𝐹 = 𝐺 → ⟨ 𝐹 , 𝐻 ⟩ = ⟨ 𝐺 , 𝐻 ⟩ )
24 23 breq2d ⊢ ( 𝐹 = 𝐺 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
25 24 biimprd ⊢ ( 𝐹 = 𝐺 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
26 22 25 syl6 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
27 26 impd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐵 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
28 18 27 syl5 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐵 = 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
29 28 expd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 𝐵 = 𝐶 → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
30 8 29 mpdd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
31 opeq1 ⊢ ( 𝐴 = 𝐶 → ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐶 , 𝐶 ⟩ )
32 31 breq2d ⊢ ( 𝐴 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ) )
33 32 anbi1d ⊢ ( 𝐴 = 𝐶 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ) )
34 31 breq1d ⊢ ( 𝐴 = 𝐶 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ↔ ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ) )
35 34 anbi1d ⊢ ( 𝐴 = 𝐶 → ( ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ↔ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ) )
36 33 35 3anbi12d ⊢ ( 𝐴 = 𝐶 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
37 36 imbi1d ⊢ ( 𝐴 = 𝐶 → ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ↔ ( ( ( 𝐵 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
38 30 37 imbitrrid ⊢ ( 𝐴 = 𝐶 → ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
39 simp12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
40 btwndiff ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) )
41 3 39 5 40 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) )
42 simpl11 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
43 simpl23 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
44 simpl32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
45 simpl21 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
46 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
47 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) )
48 42 43 44 45 46 47 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) )
49 anass ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) ↔ ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) ) )
50 anass ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ 𝐴 ≠ 𝐶 ) ↔ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) )
51 simplrl ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ )
52 51 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ )
53 simplll ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ )
54 53 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ )
55 52 54 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) )
56 simpr2l ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ )
57 56 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ )
58 simpllr ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ )
59 58 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ )
60 3 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝑁 ∈ ℕ )
61 20 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
62 simplrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) )
63 5 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
64 simplrl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
65 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ↔ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) )
66 60 61 62 63 64 65 syl122anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ( ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ↔ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) )
67 59 66 mpbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ )
68 57 67 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) )
69 simprr3 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
70 55 68 69 3jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) )
71 70 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
72 simpl11 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
73 simpl12 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
74 simpl21 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
75 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) )
76 simpl22 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
77 simpl23 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
78 simpl32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
79 simprr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) )
80 simpl33 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) )
81 brofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝑒 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐺 ⟩ , ⟨ 𝑓 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
82 72 73 74 75 76 77 78 79 80 81 syl333anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝑒 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐺 ⟩ , ⟨ 𝑓 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
83 71 82 sylibrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ⟨ ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝑒 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐺 ⟩ , ⟨ 𝑓 , 𝐻 ⟩ ⟩ ) )
84 5segofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝑒 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐺 ⟩ , ⟨ 𝑓 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) )
85 72 73 74 75 76 77 78 79 80 84 syl333anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝑒 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐺 ⟩ , ⟨ 𝑓 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) )
86 83 85 syland ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) )
87 simpr1l ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
88 87 adantr ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
89 51 adantr ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ )
90 88 89 jca ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ) )
91 simpr1r ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ )
92 91 adantr ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ )
93 53 adantr ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ )
94 90 92 93 jca32 ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ) ∧ ( 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ) )
95 simpl13 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
96 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ) )
97 72 73 95 74 75 96 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ) )
98 simpl31 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
99 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) → 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) )
100 72 77 98 78 79 99 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) → 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) )
101 97 100 anim12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ) ∧ ( 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ∧ 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) ) )
102 94 101 syl5 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) ) )
103 102 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) )
104 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ↔ 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ) )
105 72 74 95 75 104 syl13anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ↔ 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ) )
106 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ↔ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) )
107 72 78 98 79 106 syl13anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ↔ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) )
108 105 107 anbi12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ) )
109 108 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( ( 𝐶 Btwn ⟨ 𝐵 , 𝑒 ⟩ ∧ 𝐺 Btwn ⟨ 𝐹 , 𝑓 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ) )
110 103 109 mpbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) )
111 58 ad2antrl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ )
112 72 78 79 74 75 65 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ↔ ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ) )
113 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ↔ ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ) )
114 72 74 75 78 79 113 syl122anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝑒 ⟩ Cgr ⟨ 𝐺 , 𝑓 ⟩ ↔ ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ) )
115 112 114 bitrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ↔ ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ) )
116 115 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ↔ ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ) )
117 111 116 mpbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ )
118 simpr2r ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ )
119 118 ad2antrl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ )
120 72 95 74 98 78 119 cgrcomlrand ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ )
121 117 120 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ ) )
122 simprr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ )
123 simpr3r ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ )
124 123 ad2antrl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ )
125 122 124 jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
126 110 121 125 3jca ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) ) → ( ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) )
127 126 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ( ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
128 brofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
129 72 75 74 95 76 79 78 98 80 128 syl333anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐶 Btwn ⟨ 𝑒 , 𝐵 ⟩ ∧ 𝐺 Btwn ⟨ 𝑓 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝐺 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐹 ⟩ ) ∧ ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
130 127 129 sylibrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ) )
131 simplrr ⊢ ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → 𝐶 ≠ 𝑒 )
132 131 adantr ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝐶 ≠ 𝑒 )
133 132 necomd ⊢ ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝑒 ≠ 𝐶 )
134 133 a1i ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → 𝑒 ≠ 𝐶 ) )
135 130 134 jcad ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ( ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ∧ 𝑒 ≠ 𝐶 ) ) )
136 5segofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ∧ 𝑒 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
137 72 75 74 95 76 79 78 98 80 136 syl333anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑒 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑓 , 𝐺 ⟩ , ⟨ 𝐹 , 𝐻 ⟩ ⟩ ∧ 𝑒 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
138 135 137 syld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
139 138 expd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) → ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
140 139 adantrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ 𝐴 ≠ 𝐶 ) → ( ⟨ 𝑒 , 𝐷 ⟩ Cgr ⟨ 𝑓 , 𝐻 ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
141 86 140 mpdd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ) ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
142 50 141 biimtrrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
143 49 142 biimtrrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) ∧ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
144 143 expd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
145 144 anassrs ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
146 145 rexlimdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐺 Btwn ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐺 , 𝑓 ⟩ Cgr ⟨ 𝐶 , 𝑒 ⟩ ) → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
147 48 146 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) ∧ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
148 147 expd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) → ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
149 148 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑒 ⟩ ∧ 𝐶 ≠ 𝑒 ) → ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
150 41 149 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐶 ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
151 150 expd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 𝐴 ≠ 𝐶 → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
152 151 com3r ⊢ ( 𝐴 ≠ 𝐶 → ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
153 38 152 pm2.61ine ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐺 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
154 1 153 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ InnerFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )