---

Step * of Lemma in-hull-unique2

∀[g:OrientedPlane]. ∀[xs:{xs:Point List| geo-general-position(g;xs)} ]. ∀[i,j,k:ℕ||xs||].
  (j = k ∈ ℤ) supposing (ki ∈ Hull(xs) and (¬(k = i ∈ ℤ)) and ji ∈ Hull(xs) and (¬(j = i ∈ ℤ)))
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. ¬(j = i ∈ ℤ)
7. ∀k:ℕ||xs||. ((¬(k = j ∈ ℤ)) ⇒ (¬(k = i ∈ ℤ)) ⇒ (↑k L ji))
8. ¬(k = i ∈ ℤ)
9. ∀k@0:ℕ||xs||. ((¬(k@0 = k ∈ ℤ)) ⇒ (¬(k@0 = i ∈ ℤ)) ⇒ (↑k@0 L ki))
10. ¬(j = k ∈ ℤ)
11. ↑k L ji
12. ↑j L ki
⊢ 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  (ki  \mmember{}  Hull(xs)  and  (\mneg{}(k  =  i))  and  ji  \mmember{}  Hull(xs)  and  (\mneg{}(j  =  i)))


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