---

Step * of Lemma left-test_wf

∀[g:OrientedPlane]. ∀[xs:{xs:Point List| geo-general-position(g;xs)} ]. ∀[i:ℕ||xs||]. ∀[j:{j:ℕ||xs||| ¬(i = j ∈ ℤ)} ].
∀[k:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ].
  (i L jk ∈ 𝔹)
BY
{ (Auto THEN Unfold `left-test` 0 THEN MemCD THEN Try (MemTypeCD) THEN Auto THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `left-test`  0  THEN  MemCD  THEN  Try  (MemTypeCD)  THEN  Auto  THEN  EAuto  1)

---

Home Index