---

Step * of Lemma in-hull-unique3

∀[g:OrientedPlane]. ∀[xs:{xs:Point List| geo-general-position(g;xs)} ]. ∀[i,j,k:ℕ||xs||].
  ((((((¬(j = k ∈ ℤ)) ∧ (¬(j = i ∈ ℤ))) ∧ (¬(k = i ∈ ℤ))) ∧ jk ∈ Hull(xs)) ∧ ji ∈ Hull(xs)) ⇒ False)
BY
{ (((UnivCD THENA Auto) THEN ExRepD) THEN InstLemma `in-hull-unique1` [⌜g⌝;⌜xs⌝;⌜j⌝;⌜k⌝;⌜i⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  ExRepD)
  THEN  InstLemma  `in-hull-unique1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}xs\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index