Theorem btwnconn1lem13 35071

Description: Lemma for btwnconn1 35073. Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013.)

Assertion

Ref	Expression
btwnconn1lem13	⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))

Proof of Theorem btwnconn1lem13

Dummy variables 𝑒 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ne 2942	. . 3 ⊢ (𝐶 ≠ 𝑐 ↔ ¬ 𝐶 = 𝑐)
2		simp2rl 1243	. . . . . . . . . 10 ⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
3	2	adantr 482	. . . . . . . . 9 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
4		simp2ll 1241	. . . . . . . . . 10 ⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐷 Btwn ⟨𝐴, 𝑐⟩)
5	4	adantr 482	. . . . . . . . 9 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → 𝐷 Btwn ⟨𝐴, 𝑐⟩)
6	3, 5	jca 513	. . . . . . . 8 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ 𝐷 Btwn ⟨𝐴, 𝑐⟩))
7		simpl1 1192	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑁 ∈ ℕ)
8		simprl1 1219	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐶 ∈ (𝔼‘𝑁))
9		simpl2 1193	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐴 ∈ (𝔼‘𝑁))
10		simprrl 780	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑑 ∈ (𝔼‘𝑁))
11		btwncom 34986	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐴, 𝑑⟩ ↔ 𝐶 Btwn ⟨𝑑, 𝐴⟩))
12	7, 8, 9, 10, 11	syl13anc 1373	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (𝐶 Btwn ⟨𝐴, 𝑑⟩ ↔ 𝐶 Btwn ⟨𝑑, 𝐴⟩))
13		simprl2 1220	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐷 ∈ (𝔼‘𝑁))
14		simprl3 1221	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑐 ∈ (𝔼‘𝑁))
15		btwncom 34986	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐷 Btwn ⟨𝑐, 𝐴⟩))
16	7, 13, 9, 14, 15	syl13anc 1373	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (𝐷 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐷 Btwn ⟨𝑐, 𝐴⟩))
17	12, 16	anbi12d 632	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → ((𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ 𝐷 Btwn ⟨𝐴, 𝑐⟩) ↔ (𝐶 Btwn ⟨𝑑, 𝐴⟩ ∧ 𝐷 Btwn ⟨𝑐, 𝐴⟩)))
18	6, 17	imbitrid 243	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → (𝐶 Btwn ⟨𝑑, 𝐴⟩ ∧ 𝐷 Btwn ⟨𝑐, 𝐴⟩)))
19		axpasch 28199	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn ⟨𝑑, 𝐴⟩ ∧ 𝐷 Btwn ⟨𝑐, 𝐴⟩) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)))
20	7, 10, 14, 9, 8, 13, 19	syl132anc 1389	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → ((𝐶 Btwn ⟨𝑑, 𝐴⟩ ∧ 𝐷 Btwn ⟨𝑐, 𝐴⟩) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)))
21	18, 20	syld 47	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)))
22	21	imp 408	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))
23		simpll1 1213	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
24	14	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑐 ∈ (𝔼‘𝑁))
25	8	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
26	10	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑑 ∈ (𝔼‘𝑁))
27		axsegcon 28185	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩))
28	23, 24, 25, 25, 26, 27	syl122anc 1380	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩))
29		simpr 486	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁))
30		axsegcon 28185	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))
31	23, 26, 25, 25, 29, 30	syl122anc 1380	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))
32		reeanv 3227	. . . . . . . . 9 ⊢ (∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)) ↔ (∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))
33	28, 31, 32	sylanbrc 584	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))
34	33	adantr 482	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) → ∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))
35	7	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
36		simprl 770	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
37		simprr 772	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) → 𝑟 ∈ (𝔼‘𝑁))
38		axsegcon 28185	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ (𝑟 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))
39	35, 36, 37, 37, 36, 38	syl122anc 1380	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))
40	39	adantr 482	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ ((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))
41		simp-4l 782	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → (𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
42		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)))
43	42	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)))
44	10	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑑 ∈ (𝔼‘𝑁))
45		simprrr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁))
46	45	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
47		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁))
48	44, 46, 47	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)))
49	43, 48	jca 513	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))))
50		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑝 ∈ (𝔼‘𝑁))
51		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑞 ∈ (𝔼‘𝑁))
52		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑟 ∈ (𝔼‘𝑁))
53	50, 51, 52	3jca 1129	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑞 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)))
54	41, 49, 53	3jca 1129	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) → ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑞 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))))
55		simp1ll 1237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐴 ≠ 𝐵)
56	55	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) → 𝐴 ≠ 𝐵)
57	56	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → 𝐴 ≠ 𝐵)
58		simp1lr 1238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐵 ≠ 𝐶)
59	58	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) → 𝐵 ≠ 𝐶)
60	59	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → 𝐵 ≠ 𝐶)
61		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) → 𝐶 ≠ 𝑐)
62	61	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → 𝐶 ≠ 𝑐)
63	57, 60, 62	3jca 1129	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐))
64		simpl1r 1226	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩))
65	64	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩))
66	63, 65	jca 513	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)))
67		simpll2 1214	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) → ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)))
68	67	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)))
69		simpl3l 1229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → (𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩))
70	69	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩))
71		simpl3r 1230	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) → (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))
72	71	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))
73	70, 72	jca 513	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩)))
74	66, 68, 73	3jca 1129	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 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⟨𝐷, 𝐵⟩))))
75		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))
76		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩))
77		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))
78		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))
79	76, 77, 78	3jca 1129	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)) → ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)))
80	74, 75, 79	jca32 517	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 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 ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩)))))
81		btwnconn1lem12 35070	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑞 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))))) → 𝐷 = 𝑑)
82	54, 80, 81	syl2an 597	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ (((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩))) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))) → 𝐷 = 𝑑)
83	82	an4s 659	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ ((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))) ∧ (𝑞 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn ⟨𝑝, 𝑞⟩ ∧ ⟨𝑟, 𝑞⟩Cgr⟨𝑟, 𝑝⟩))) → 𝐷 = 𝑑)
84	40, 83	rexlimddv 3162	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ ((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))) → 𝐷 = 𝑑)
85	84	an4s 659	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) ∧ ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ ((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)))) → 𝐷 = 𝑑)
86	85	exp32 422	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) → ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) → (((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)) → 𝐷 = 𝑑)))
87	86	rexlimdvv 3211	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) → (∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn ⟨𝑐, 𝑝⟩ ∧ ⟨𝐶, 𝑝⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑟⟩ ∧ ⟨𝐶, 𝑟⟩Cgr⟨𝐶, 𝑒⟩)) → 𝐷 = 𝑑))
88	34, 87	mpd 15	. . . . . 6 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) → 𝐷 = 𝑑)
89	88	an4s 659	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ (𝑒 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝑒 Btwn ⟨𝐷, 𝑑⟩))) → 𝐷 = 𝑑)
90	22, 89	rexlimddv 3162	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ 𝐶 ≠ 𝑐)) → 𝐷 = 𝑑)
91	90	expr 458	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩)))) → (𝐶 ≠ 𝑐 → 𝐷 = 𝑑))
92	1, 91	biimtrrid 242	. 2 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩)))) → (¬ 𝐶 = 𝑐 → 𝐷 = 𝑑))
93	92	orrd 862	1 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∃wrex 3071  ⟨cop 4635   class class class wbr 5149  ‘cfv 6544  ℕcn 12212  𝔼cee 28146   Btwn cbtwn 28147  Cgrccgr 28148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-ee 28149  df-btwn 28150  df-cgr 28151  df-ofs 34955  df-colinear 35011  df-ifs 35012  df-cgr3 35013  df-fs 35014

This theorem is referenced by:  btwnconn1lem14  35072