---

Step * of Lemma geo-general-position-implies

∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i,j,k:ℕ||xs||.
  ((¬(i = j ∈ ℤ)) ⇒ (¬(k = i ∈ ℤ)) ⇒ (¬(k = j ∈ ℤ)) ⇒ xs[i] # xs[j]xs[k])
BY
{ 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 = i ∈ ℤ)
8. ¬(k = j ∈ ℤ)
⊢ xs[i] # xs[j]xs[k]

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}xs:\{xs:Point  List|  geo-general-position(g;xs)\}  .  \mforall{}i,j,k:\mBbbN{}||xs||.
    ((\mneg{}(i  =  j))  {}\mRightarrow{}  (\mneg{}(k  =  i))  {}\mRightarrow{}  (\mneg{}(k  =  j))  {}\mRightarrow{}  xs[i]  \#  xs[j]xs[k])


By

---

Latex:
Auto

---

Home Index