---

Step * 1 1 1 1 of Lemma in-hull-next2


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. 2 < ||xs||
8. x : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} 
9. ∀y:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} . ((¬(x = y ∈ ℤ)) ⇒ (↑x L iy))
10. k : ℕ||xs||
11. ¬(k = x ∈ ℤ)
12. ¬(k = i ∈ ℤ)
13. k = j ∈ ℤ
14. ¬(x = i ∈ ℤ)
⊢ ↑j L xi
BY
{ (((DSetVars THEN (D 7 With ⌜x⌝  THENA Auto)) THEN RepeatFor 2 ((D -1 THENA Auto)))
   THEN RWO  "left-test-symmetry" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  xs  :  \{xs:Point  List|  geo-general-position(g;xs)\} 
3.  i  :  \mBbbN{}||xs||
4.  j  :  \mBbbN{}||xs||
5.  \mneg{}(i  =  j)
6.  ij  \mmember{}  Hull(xs)
7.  2  <  ||xs||
8.  x  :  \{k:\mBbbN{}||xs|||  (\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j))\} 
9.  \mforall{}y:\{k:\mBbbN{}||xs|||  (\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j))\}  .  ((\mneg{}(x  =  y))  {}\mRightarrow{}  (\muparrow{}x  L  iy))
10.  k  :  \mBbbN{}||xs||
11.  \mneg{}(k  =  x)
12.  \mneg{}(k  =  i)
13.  k  =  j
14.  \mneg{}(x  =  i)
\mvdash{}  \muparrow{}j  L  xi


By

---

Latex:
(((DSetVars  THEN  (D  7  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto))  THEN  RepeatFor  2  ((D  -1  THENA  Auto)))
  THEN  RWO    "left-test-symmetry"  0
  THEN  Auto)

---

Home Index