Metamath Proof Explorer

Theorem btwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn3 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 btwndiff ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) )
5 1 2 3 4 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) )
6 simprlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 ≠ 𝑝 )
7 6 necomd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝑝 ≠ 𝐴 )
8 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
9 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
11 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
14 8 10 9 12 13 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐷 , 𝐴 ⟩ )
15 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ )
16 8 12 10 9 11 14 15 btwnexch3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝐵 , 𝑝 ⟩ )
17 8 9 10 11 16 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑝 , 𝐵 ⟩ )
18 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
19 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
20 8 18 9 12 19 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ )
21 8 12 18 9 11 20 15 btwnexch3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝐶 , 𝑝 ⟩ )
22 8 9 18 11 21 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑝 , 𝐶 ⟩ )
23 7 17 22 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → ( 𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐵 ⟩ ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐶 ⟩ ) )
24 23 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐵 ⟩ ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐶 ⟩ ) ) )
25 btwnconn2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐵 ⟩ ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐶 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
26 8 11 9 10 18 25 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐵 ⟩ ∧ 𝐴 Btwn ⟨ 𝑝 , 𝐶 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
27 24 26 syld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
28 27 expd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
29 28 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐷 , 𝑝 ⟩ ∧ 𝐴 ≠ 𝑝 ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
30 5 29 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )