Metamath Proof Explorer

Theorem seglecgr12im

Description: Substitution law for segment comparison under congruence. Theorem 5.6 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 simprrl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
2 simprlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ )
3 simpl11 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
4 simpl21 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simpl22 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simpl32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpl33 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) )
9 cgrxfr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) ) )
10 3 4 5 6 7 8 9 syl132anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) ) )
11 10 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) ) )
12 1 2 11 mp2and ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) )
13 anass ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
14 simpl11 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
15 simpl21 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpl22 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simpl32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
19 simprr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
20 simpl33 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) )
21 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) )
22 14 15 16 17 18 19 20 21 syl133anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) )
23 22 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) )
24 df-3an ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ↔ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) )
25 simpl23 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
26 simpl31 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
27 simpl12 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
28 simpl13 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
29 simpr1l ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )
30 simpr2r ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
31 14 27 28 25 26 15 16 29 30 cgrtr4and ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
32 simpr31 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ )
33 14 25 26 15 16 18 19 31 32 cgrtrand ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ )
34 24 33 sylan2br ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) ) ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ )
35 34 expr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑧 , 𝐻 ⟩ ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) )
36 23 35 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) )
37 36 anim2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) → ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
38 13 37 sylanb ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) → ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
39 38 an32s ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) → ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
40 39 reximdva ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ( ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝑧 , 𝐻 ⟩ ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
41 12 40 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) )
42 41 expr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
43 42 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
44 43 rexlimdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
45 simp11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
46 simp12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
47 simp13 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
48 simp21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
49 simp22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
50 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
51 45 46 47 48 49 50 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
52 51 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
53 simp23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
54 simp31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
55 simp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
56 simp33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) )
57 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
58 45 53 54 55 56 57 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
59 58 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝑧 ⟩ ) ) )
60 44 52 59 3imtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ) )
61 60 exp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ → ( ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ) ) ) )
62 61 3impd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ) → ⟨ 𝐸 , 𝐹 ⟩ Seg≤ ⟨ 𝐺 , 𝐻 ⟩ ) )