---

Step * of Lemma in-hull-unique1

∀[g:OrientedPlane]. ∀[xs:{xs:Point List| geo-general-position(g;xs)} ]. ∀[i,j,k:ℕ||xs||].
  (j = k ∈ ℤ) supposing (ik ∈ Hull(xs) and (¬(i = k ∈ ℤ)) and ij ∈ Hull(xs) and (¬(i = j ∈ ℤ)))
BY
{ (Auto
   THEN (SupposeNot THENA Auto)
   THEN (Unfold `in-hull` -4 THEN (InstHyp [⌜k⌝] (-4)⋅ THENA Auto))
   THEN Unfold `in-hull` -3
   THEN (InstHyp [⌜j⌝] (-3)⋅ THENA Auto)) }

1
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. i : ℕ||xs||
4. j : ℕ||xs||
5. k : ℕ||xs||
6. ¬(i = j ∈ ℤ)
7. ∀k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ⇒ (¬(k = j ∈ ℤ)) ⇒ (↑k L ij))
8. ¬(i = k ∈ ℤ)
9. ∀k@0:ℕ||xs||. ((¬(k@0 = i ∈ ℤ)) ⇒ (¬(k@0 = k ∈ ℤ)) ⇒ (↑k@0 L ik))
10. ¬(j = k ∈ ℤ)
11. ↑k L ij
12. ↑j L ik
⊢ j = k ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[g:OrientedPlane].  \mforall{}[xs:\{xs:Point  List|  geo-general-position(g;xs)\}  ].  \mforall{}[i,j,k:\mBbbN{}||xs||].
    (j  =  k)  supposing  (ik  \mmember{}  Hull(xs)  and  (\mneg{}(i  =  k))  and  ij  \mmember{}  Hull(xs)  and  (\mneg{}(i  =  j)))


By

---

Latex:
(Auto
  THEN  (SupposeNot  THENA  Auto)
  THEN  (Unfold  `in-hull`  -4  THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto))
  THEN  Unfold  `in-hull`  -3
  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))

---

Home Index