---

Step * of Lemma in-hull-unique-next

∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i,j:ℕ||xs||.
  ((¬(i = j ∈ ℤ)) ⇒ ij ∈ Hull(xs) ⇒ (∃!k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ∧ ki ∈ Hull(xs))))
BY
{ (InstLemma `in-hull-next` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN UnfoldTopAb 0
   THEN ParallelLast'
   THEN Auto) }

1
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. k : ℕ||xs||
8. ¬(k = i ∈ ℤ)
9. ki ∈ Hull(xs)
10. ¬(k = i ∈ ℤ)
11. ki ∈ Hull(xs)
12. y : ℕ||xs||
13. ¬(y = i ∈ ℤ)
14. yi ∈ Hull(xs)
⊢ y = k ∈ ℕ||xs||

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}xs:\{xs:Point  List|  geo-general-position(g;xs)\}  .  \mforall{}i,j:\mBbbN{}||xs||.
    ((\mneg{}(i  =  j))  {}\mRightarrow{}  ij  \mmember{}  Hull(xs)  {}\mRightarrow{}  (\mexists{}!k:\mBbbN{}||xs||.  ((\mneg{}(k  =  i))  \mwedge{}  ki  \mmember{}  Hull(xs))))


By

---

Latex:
(InstLemma  `in-hull-next`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  UnfoldTopAb  0
  THEN  ParallelLast'
  THEN  Auto)

---

Home Index